[Haskell-cafe] type level program
Markus Läll
markus.l2ll at gmail.com
Mon Oct 25 12:45:07 EDT 2010
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
>
More information about the Haskell-Cafe
mailing list