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