Not exactly answering your question, but just in case you hadn't
checked, there are a few packages for type level natural numbers on
hackage, which do the same things as the program below. The packages
are:
- type-level-natural-number and co by Gregory Crosswhite, and
- type-level-numers by Alexey Khudyakov (which does type-level binary
encoding(!) for natural numbers)
As for the terminology, I can't tell..
Out of intrest, is this kind of type-level stuff to prove things about
your container types and operations on them?
--
Markus Läll
On Mon, Oct 25, 2010 at 12:52 PM, 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe