Over on comp.lang.lisp we have a comparison of between the type systems of lisp and ML. I don't know enough about ML to know whether it is or isn't up to the challenge, but here's a teaser of how you could go about it in Haskell. First off, we need a data type that knows about the range of possible values for its integral argument. And then we need to be able to exponentiate the range...
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Range where
data Range val low high = R val deriving (Eq, Show)
x = R 3 :: Range Integer One Three
y = R 2 :: Range Integer One Two
main = print $ expt x y
data Zero
data Succ n
type One = Succ Zero
type Two = Succ (Succ Zero)
type Three = Succ (Succ (Succ Zero))
type Four = Succ (Succ (Succ (Succ Zero)))
class AddT a b c | a b -> c where addt :: a->b->c
instance AddT Zero b b
instance AddT a b c => AddT (Succ a) b (Succ c)
class MulT a b c | a b -> c where mult :: a->b->c
instance MulT Zero b Zero
instance (MulT a b c, AddT b c d) => MulT (Succ a) b d
class PowT a b c | a b -> c where powt :: a->b->c
instance PowT a Zero One
instance (PowT a b c, MulT a c d) => PowT a (Succ b) d
class AddR l1 h1 l2 h2 l3 h3 | l1 l2 -> l3, h1 h2 -> h3 where
(.+) :: Range Integer l1 h1 -> Range Integer l2 h2 -> Range Integer l3 h3
instance (AddT l1 l2 l3, AddT h1 h2 h3) => AddR l1 h1 l2 h2 l3 h3 where
(R x) .+ (R y) = R (x+y)
class MulR l1 h1 l2 h2 l3 h3 | l1 l2 -> l3, h1 h2 -> h3 where
(.*) :: Range Integer l1 h1 -> Range Integer l2 h2 -> Range Integer l3 h3
instance (MulT l1 l2 l3, MulT h1 h2 h3) => MulR l1 h1 l2 h2 l3 h3 where
(R x) .* (R y) = R (x*y)
class PowR l1 h1 l2 h2 l3 h3 | l1 l2 -> l3, h1 h2 -> h3 where
expt :: Range Integer l1 h1 -> Range Integer l2 h2 -> Range Integer l3 h3
instance (PowT l1 l2 l3, PowT h1 h2 h3) => PowR l1 h1 l2 h2 l3 h3 where
expt (R x) (R y) = R (x^y)
$ ghci net.hs ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.6, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help. Loading package base ... linking ... done. [1 of 1] Compiling Range ( net.hs, interpreted ) Ok, modules loaded: Range. *Range> :t x x :: Range Integer One Three *Range> :t y y :: Range Integer One Two *Range> :t expt x y expt x y :: Range Integer (Succ Zero) (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))) *Range>
...Looks like the type checker can compute that 3 squared is 9. Good. Now for optimizing the results by placing the values in small machine words...
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Range where
import Data.Word
newtype Range val low high = R val deriving (Eq, Show)
a = R 0 :: Range Word8 Zero Two
b = R 1 :: Range Word8 Zero Two
main = print $ a .+ b
data Zero
data Succ n
type One = Succ Zero
type Two = Succ (Succ Zero)
type Four = Succ (Succ (Succ (Succ Zero)))
class AddT a b c | a b -> c
instance AddT Zero b b
instance AddT a b c => AddT (Succ a) b (Succ c)
class AddR a b inl inh outl outh | inl -> outl,
inh -> outh,
inl inh -> a,
outl outh -> b where
(.+) :: Range a inl inh -> Range a inl inh -> Range b outl outh
instance (AddT inl inl outl, AddT inh inh outh,
Lookup inl inh a, Lookup outl outh b,
Num a, Num b, Integral a, Integral b)
=> AddR a b inl inh outl outh where
(R x) .+ (R y) = R (fromIntegral (x+y))
class Lookup a b c | a b -> c
instance Lookup Zero Two Word8
instance Lookup Zero Four Word16
...and the test...
___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.6, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help. Loading package base ... linking ... done. [1 of 1] Compiling Range ( optimized.hs, interpreted ) Ok, modules loaded: Range. *Range> :t a a :: Range Word8 Zero Two *Range> :t b b :: Range Word8 Zero Two *Range> :t a .+ b a .+ b :: Range Word16 Zero (Succ (Succ (Succ (Succ Zero)))) *Range>
...That's supposed to show that you can stick values in the range of zero to two in a Word8, but values in the range of zero to four require a Word16. Of course, you'll want to choose better cutoffs for deciding which ranges fit into which Words and you'll want to replace the unary numbers with something like Number-parameterized types. See also, these fine papers...
