[Haskell-cafe] A type level puzzle
Tom Ellis
tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk
Fri Aug 14 21:46:35 UTC 2015
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
More information about the Haskell-Cafe
mailing list