<br><br>On Friday, August 14, 2015, Tom Ellis <<a href="mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk">tom-lists-haskell-cafe-2013@jaguarpaw.co.uk</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">For the type level gurus:<br>
<br>
I would like to define types<br>
<br>
    Sum :: [Field] -> *<br>
<br>
    (:::) :: String -> * -> Field<br>
<br>
used like this<br>
<br>
    Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]<br>
<br>
(I hope this makes sense.  I'm not quite familiar with the syntax.)<br>
<br>
such that<br>
<br>
    Sum '[ s1 ::: a1, ... ]<br>
<br>
unifies with<br>
<br>
    Sum '[ s1 ::: b1, ... ]<br>
<br>
to give<br>
<br>
    Sum '[ s1 ::: c1, ... ]<br>
<br>
where c1 is the unification of a1 and b1.  If sn is absent from exactly one<br>
of the unificands then its type is copied over unchanged.  If sn is absent<br>
from both then it is absent from the unification.  The types should also be<br>
invariant under permutation of the list.<br>
<br>
This is perhaps a bit obscure so I'll explain the application.  This is<br>
intended for the sumtype equivalent of a record type, so if we have<br>
<br>
    Sum '[ "foo" ::: a, "bar" ::: b ]<br>
<br>
and<br>
<br>
    Sum '[ "foo" ::: a, "baz" ::: c ]<br>
<br>
then I take take the sum of these sums and get something of type<br>
<br>
    Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ]<br>
<br>
If it makes it easier than I am happy for<br>
<br>
    Sum '[ s1 ::: a1, ... ]<br>
<br>
to unify with<br>
<br>
    forall ak. Sum '[ s1 ::: a1, ..., sk ::: ak ]<br>
<br>
This is justified by<br>
<br>
    forall b. Either a b<br>
<br>
being isomorphic to a.<br>
<br>
Is such a type possible?  If so my next question will be about how to type<br>
deconstructors of such things, but let's start with a small first step!<br>
<br>
Thanks,<br>
<br>
Tom</blockquote><div><br></div><div><br></div>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:<div><br></div><div><<a href="http://hackage.haskell.org/package/Frames-0.1.2.1/docs/Frames-CoRec.html">http://hackage.haskell.org/package/Frames-0.1.2.1/docs/Frames-CoRec.html</a>><br><div><br></div><div>I make rather heavy use of this kind of programming, and have thus far found it to scale up quite well.</div><div><br></div><div>Anthony</div><div> </div></div>