[Haskell-cafe] type level program

[Markus Läll]

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 <patrick.browne at dit.ie> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>