[Haskell-cafe] type level program
Patrick Browne
patrick.browne at dit.ie
Mon Oct 25 05:52:41 EDT 2010
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
More information about the Haskell-Cafe
mailing list