[Haskell-cafe] A type level puzzle
Anthony Cowley
acowley at seas.upenn.edu
Sat Aug 15 14:56:55 UTC 2015
On Friday, August 14, 2015, Tom Ellis <
tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> wrote:
> For the type level gurus:
>
> I would like to define types
>
> Sum :: [Field] -> *
>
> (:::) :: String -> * -> Field
>
> used like this
>
> Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]
>
> (I hope this makes sense. I'm not quite familiar with the syntax.)
>
> such that
>
> Sum '[ s1 ::: a1, ... ]
>
> unifies with
>
> Sum '[ s1 ::: b1, ... ]
>
> to give
>
> Sum '[ s1 ::: c1, ... ]
>
> where c1 is the unification of a1 and b1. If sn is absent from exactly one
> of the unificands then its type is copied over unchanged. If sn is absent
> from both then it is absent from the unification. The types should also be
> invariant under permutation of the list.
>
> This is perhaps a bit obscure so I'll explain the application. This is
> intended for the sumtype equivalent of a record type, so if we have
>
> Sum '[ "foo" ::: a, "bar" ::: b ]
>
> and
>
> Sum '[ "foo" ::: a, "baz" ::: c ]
>
> then I take take the sum of these sums and get something of type
>
> Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]
>
> If it makes it easier than I am happy for
>
> Sum '[ s1 ::: a1, ... ]
>
> to unify with
>
> forall ak. Sum '[ s1 ::: a1, ..., sk ::: ak ]
>
> This is justified by
>
> forall b. Either a b
>
> being isomorphic to a.
>
> Is such a type possible? If so my next question will be about how to type
> deconstructors of such things, but let's start with a small first step!
>
> Thanks,
>
> Tom
This won't get you everything you mention out of the box, but I expect you
can piece together the last bits of what you want with the exception that
type inference will be limited. Here are basic open sums, conversions
between sums and products, and matching against sums:
<http://hackage.haskell.org/package/Frames-0.1.2.1/docs/Frames-CoRec.html>
I make rather heavy use of this kind of programming, and have thus far
found it to scale up quite well.
Anthony
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150815/3276acd9/attachment.html>
More information about the Haskell-Cafe
mailing list