>This will only work for terminating programs!
Interesting point, but thats because all the operations are at
the type level - therefore if a type is unknown at compile time
we cannot produce a program.
With this type class stuff values can depend on types, but
not the other way around. You can
The append example is meant to make a general point about
the connection between dependent types and Haskell with
extensions.
I know that the example itself is rather trivial, and
DML/index types, Omega, Haskell+GAD and Chameleon might
seem as too big canons for a rather small target.
> Second
Actually the data statement wasnt quite right:
data Cons a b = Cons a b
Would work, but now there is nothing keeping each
element in the list as the same type,
I guess we could add a class to constrain to a normal list,,,
class List l x
instance List Nil x
instance List l x => List (Cons x l) x
Just a couple of quick points...
Why store the length along with the list, the length is stored
using type level naturals (Succ | Zero) but these are identical
to the recursion pattern in a List (Cons | Nil) - therefore it
is no less work than having a length function which converts
from one to th
There's a potentially confusing typo.
> append Nil ys = Nil
should be replaced by
append Nil ys = ys
Thanks to Ketil for pointing this out.
Martin
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
-- append.hs
-- append in Haskell
data List a = Nil
| Cons a (List a)
append :: List a -> List a -> List a
a
