<p dir="ltr">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)</p>
<p dir="ltr">If you want to learn more about dependent types, looking at Idris or Agda is what you actually want.</p>
<p dir="ltr">I would avoid it, Haskell's type system is not a nice programming language to work with </p>
<div class="gmail_quote">On Aug 15, 2015 10:13 AM, "Tom Ellis" <<a href="mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk">tom-lists-haskell-cafe-2013@jaguarpaw.co.uk</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Sat, Aug 15, 2015 at 02:35:53PM +0200, Silvio Frischknecht wrote:<br>
> I'm not going to do the whole thing for you but I can help start you off.<br>
><br>
> The type level string you think of is called Symbol. Symbol is a kind on<br>
> it's own and not (*) it has a type for every string. You can use the<br>
> functions in the following link to work with them.<br>
><br>
> <a href="https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html</a><br>
><br>
> so you might have<br>
><br>
> newtype (symbol :: Symbol) ::: value = Field value<br>
><br>
> you can basically use any typelevel combinator you want for Sum e.g.<br>
><br>
> ("foo" ::: Int) `(,)` ("bar" ::: Char) `(,)` ...<br>
><br>
> or make your own<br>
><br>
> You will have to use type families which are basically type level<br>
> functions to merge two sums.<br>
><br>
> If you run into trouble you can have a look at the following link which<br>
> does some similar things.<br>
><br>
> <a href="https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.html" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/type-level-sets-0.5/docs/Data-Type-Set.html</a><br>
><br>
><br>
> P.S. Prepare for a headache<br>
<br>
A good headache or a bad headache?  If it's hard to learn but ultimately<br>
satisfying and useful then I'm all up for it.  If it's hard to learn because<br>
Haskell doesn't really support it naturally then I'll probably avoid it.<br>
<br>
Tom<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>