[Haskell-cafe] A type level puzzle

[Esteban I. RM.]

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 Aug 15, 2015 10:13 AM, "Tom Ellis" <
tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> wrote:

> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150815/16773aa9/attachment.html>