[Haskell-cafe] Extensible Type Unification

[Leon Smith]

It finally occurred to me how to get most of what I want,  at least from a
functional perspective.    Here's a sample GADT,  with four categories of
constructor:

data Foo :: Bool -> Bool -> Bool -> Bool -> * where
    A :: Foo True b c d
    B :: Foo True b c d
    C :: Foo a True c d
    D :: Foo a b True d
    E :: Foo a b c True

Given an Eq instance,  we can easily compare two constructors for equality;
  we can put some constructors in a list and tell which categories appear
in the list,   and it plays reasonably nicely with the case coverage
analyzer,  which I think is important from a software engineering
standpoint.    For example,  this function will compile without warning:

fooVal :: Foo a b False False -> Int
fooVal  x =
   case x of
      A -> 0
      B -> 1
      C -> 2

The only thing this doesn't do that I wish it did is infer the type of
fooVal above.    Rather,  GHC  infers the type  :: Foo a b c d -> Int,
and then warns me that I'm missing cases.   But this is admittedly a
strange form of type inference,   completely alien to the Haskell
landscape,   which I realized only shortly after sending my original email.
  My original description of ranges of sets of types wasn't sufficient to
fully capture my intention.

That said,  this solution falls rather flat in several software engineering
respects.  It doesn't scale with complexity;   types quickly become
overbearing even with modest numbers of categories.    If you want to add
additional categories,   you have to modify every type constructor instance
you've ever written down.    You could mitigate some of this via the
existing type-level machinery,  but it seems a band-aid,  not a solution.

For comparison,  here is the best I had when I wrote my original email:

data Category = W | X | Y | Z

data Foo :: [Category] -> * where
    A :: (Member W ub) => Foo ub
    B :: (Member W ub) => Foo ub
    C :: (Member X ub) => Foo ub
    D :: (Member Y ub) => Foo ub
    E :: (Member Z ub) => Foo ub

class Member (a :: x) (bs :: [x])
instance Member a (a ': bs)
instance Member a bs => Member a (b ': bs)

The code is closer to what I want,  in terms of expression,  though it
mostly fails on the functional requirements.    Case analysis doesn't work,
  I can't compare two constructors without additional type annotations,
and while I can find out which categories of constructors appear in a list,
  it doesn't seem I can actually turn those contexts into many useful
things,  automatically.

So while I didn't have any trouble computing set operations over unordered
lists at the type level,   I couldn't figure out out to put it to use in
the way I wanted.    Perhaps there is a clever way to emulate unification,
 but I really like the new features that reduce the need to be clever when
it comes to type-level computation.

Best,
Leon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130208/5829f9c7/attachment.htm>