Type system computation

Over on comp.lang.lisp we have a comparison [1] 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)

...then we'll ask about the types...

$ ghci net.hs
   ___         ___ _
  / _ \ /\  /\/ __(_)
 / /_\// /_/ / /  | |      GHC Interactive, version 6.6, for Haskell 98.
/ /_\\/ __  / /___| |      http://www.haskell.org/ghc/ [2]
\____/\/ /_/\____/|_|      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/ [3]
\____/\/ /_/\____/|_|      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 [4]. See also, these fine papers...

Fun with Functional Dependencies [5]
Faking It: Simulating Dependent Types in Haskell [6]
Fun with Phantom Types [7]