[Haskell-cafe] type level program

[Patrick Browne]

Hi,
I hypothesize that at type level Haskell offers a form of equational
logic. At type level the following program[1] could be interpreted as a
first order program in equational logic where;
1)Data types represent declarations of constructors (both constants and
functions)
2)Type synonyms represent equations assigning constructors to variables
3)Each class contains a non-constructor operation signature with
dependencies
4) instances contain equations that define the operations
 (similar the term rewriting systems (TRS) of  Maude/CafeOBJ).

5):t acts as a reduction or evaluation at type level

Is the a reasonable description of this program?

Regards,
Pat

[1] From Fritz Ruehr
http://www.willamette.edu/~fruehr/haskell/evolution.html

-- static Peano constructors and numerals
data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two
type Four  = Succ Three


-- dynamic representatives for static Peanos

zero  = undefined :: Zero
one   = undefined :: One
two   = undefined :: Two
three = undefined :: Three
four  = undefined :: Four


-- addition, a la Prolog

class Add a b c | a b -> c where
  add :: a -> b -> c

instance              Add  Zero    b  b
instance Add a b c => Add (Succ a) b (Succ c)


-- multiplication, a la Prolog

class Mul a b c | a b -> c where
  mul :: a -> b -> c

instance                           Mul  Zero    b Zero
instance (Mul a b c, Add b c d) => Mul (Succ a) b d


-- factorial, a la Prolog

class Fac a b | a -> b where
  fac :: a -> b

instance                                Fac  Zero    One
instance (Fac n k, Mul (Succ n) k m) => Fac (Succ n) m

-- try, for "instance" (sorry):
-- 
--     :t fac four

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie