it is not a nice headache; doing quasi dependent types ends with lots of redundancy like implementing functions both at the type level and the value level, duplicating data types definitions (even though singletons helps there)
If you want to learn more about dependent types, looking at Idris or Agda is what you actually want.
I would avoid it, Haskell's type system is not a nice programming language to work with
On Sat, Aug 15, 2015 at 02:35:53PM +0200, Silvio Frischknecht wrote:
> I'm not going to do the whole thing for you but I can help start you off.
>
> The type level string you think of is called Symbol. Symbol is a kind on
> it's own and not (*) it has a type for every string. You can use the
> functions in the following link to work with them.
>
> https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html
>
> so you might have
>
> newtype (symbol :: Symbol) ::: value = Field value
>
> you can basically use any typelevel combinator you want for Sum e.g.
>
> ("foo" ::: Int) `(,)` ("bar" ::: Char) `(,)` ...
>
> or make your own
>
> You will have to use type families which are basically type level
> functions to merge two sums.
>
> If you run into trouble you can have a look at the following link which
> does some similar things.
>
> https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.html
>
>
> P.S. Prepare for a headache
A good headache or a bad headache? If it's hard to learn but ultimately
satisfying and useful then I'm all up for it. If it's hard to learn because
Haskell doesn't really support it naturally then I'll probably avoid it.
Tom
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe