Greg Buchholz wrote:
Keean Schupke wrote:
Haskell is not dependantly typed, so cannot deal with types that "depend" on values.
Can anyone recommend a nice dependently typed language to play with? Cayenne, Epigram, other?
I have refactored your code into a type level Haskell program. This has the nice advantage that it is extensible. You can add a new primitive to the language as: data PrimName primName :: PrimName primName = undefined instance Apply PrimName a b where apply _ a = {- method implementing primName -} Programs are assembled as types like: fac4 = lit nul `o` lit suc `o` lit (dup `o` pre) `o` lit mult `o` linrec Recursion requires a primitive to aviod infinite types, see definitions of times, linrec and genrec. programs are run by applying the contructed type representing the program to a stack... for example: putStrLn $ show $ apply (lit hThree `o` fac4) hNil We could have written this: putStrLn $ show $ apply fac4 (hCons hThree hNil) I have attached the debugged code, simply load into ghci, in the same directory as the HList library (download http://www.cwi.nl/~ralf/HList) as Joy.hs. ghci -fallow-overlapping-instances Joy.hs (you need the flag to get the code to run interactively, however you dont need the flag just to run 'main' to perform the factorial tests) Keean.