Leon Smith | 8 Feb 07:07 2013

Extensible Type Unification

I've been toying with some type-level programming ideas I just can't quite make work,   and it seems what I really want is a certain kind of type unification.

Basically,  I'd like to introduce two new kind operators:

kind Set as   -- a finite set of ground type terms of kind as

kind Range as = Range (Set as) (Set as)      -- a greatest lower bound and a least upper bound

A type expression of kind (Set as)  would either be a type variable of kind (Set as),  or set of *ground* type terms of kind (as).      A type expression of kind (Range as) would be a type variable
of kind (Range as),  or two type expressions of kind (Set as).   To unify ground terms of these types,  one would compute as follows:

unifySets xs ys 
   |  xs == ys  = Just xs
   |  otherwise = Nothing

unifyRanges (Range glb0 lub0) (Range glb1 lub1)
    | glb' `subset` lub' = Just (Range glb' lub')
    | otherwise          = Nothing
    glb' = glb0 `union` glb1
    lub' = lub0 `isect` lub1

I say sets of ground types,  because I have no idea what unification between sets of non-ground types would mean,  and I really don't need it.   

Among applications that came to mind,   one could use this to create a restricted IO abstraction that could tell you which kinds of actions might be taken  (read from mouse,  talk to network,  etc),   and be able to run
only those scripts that are restricted to certain resources.     Or,  one could define a singular GADT that represents messages/events decorated by various categories,   and then define functions that
only operate on selected categories of messages.    E.G. for something vaguely IRC-ish,  one could write something like:

data EventCategory
    = Channel
    | Presence
    | Information
    | Conversation

data Event :: Range EventCategory -> *  where
    ChanCreate     ::  ...  -> Event (Range (Set '[Channel])      a)
    ChanJoin       ::  ...  -> Event (Range (Set '[Channel])      a)
    ChanLeave      ::  ...  -> Event (Range (Set '[Channel])      a)
    PresAvailable  ::  ...  -> Event (Range (Set '[Presence])     a)
    PresAway       ::  ...  -> Event (Range (Set '[Presence])     a)
    WhoisQuery     ::  ...  -> Event (Range (Set '[Information])  a)
    WhoisResponse  ::  ...  -> Event (Range (Set '[Information])  a)
    Message        ::  ...  -> Event (Range (Set '[Conversation]) a)

And then be able to write functions such as

dispatch :: Event (Range a (Set '[Channel, Conversation]))  -> IO ()
dispatch e =
    case e of 
        ChanCreate{..} -> ...
        ChanJoin{..} -> ...
        ChanLeave{..} -> ...
        Message{..} -> ...

In this case,  the case analysis tool would be able to warn me if I'm missing any possible events in this dispatcher,  or  if I have extraneous events that I can't be passed (according to my type.)

Anyway,  I've been trying to see if I can't come up with something similar using existing type-level functionality in 7.6,   with little success.   (Though I'm not very experienced with type-level programming.)     If not,  might it be possible to add some kind of extensible unification mechanism,  in furtherance of type-level programming? 


Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
Leon Smith | 8 Feb 12:18 2013

Re: Extensible Type Unification

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.

Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org