[Haskell-cafe] Kleene star in types

7 May 2007

      Apologies for sending this twice. Mutt obviously outsmarted mailman and
put a useful mime type header in. Not so this one!

This email is a .lhs.
...
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
Let's implement the Kleene * in the type system. First some phantom
types:
...
data At n
data Bt n
data Ct n
data Endt
Now a chain to hold it together:
...
data Chain :: * -> * where
              Ac :: (Chain n) -> Chain (At n)
              Bc :: (Chain n) -> Chain (Bt n)
              Cc :: (Chain n) -> Chain (Ct n)
              Endc :: Chain Endt
instance Show (Chain n) where
    show (Ac n) = "Ac ~> " ++ (show n)
    show (Bc n) = "Bc ~> " ++ (show n)
    show (Cc n) = "Cc ~> " ++ (show n)
    show (Endc) = "Endc"
Now, first things first, implement identity. I don't really care about
the actual functions right now, but let's put it in anyway.
...
class IdOp a b | a -> b, b -> a where
    idOp :: a -> b
instance IdOp (Chain Endt) (Chain Endt) where
    idOp x = x
instance (IdOp (Chain l) (Chain r)) =>
    IdOp (Chain (At l)) (Chain (At r)) where
    idOp (Ac n) = Ac (idOp n)
instance (IdOp (Chain l) (Chain r)) =>
    IdOp (Chain (Bt l)) (Chain (Bt r)) where
    idOp (Bc n) = Bc (idOp n)
instance (IdOp (Chain l) (Chain r)) =>
    IdOp (Chain (Ct l)) (Chain (Ct r)) where
    idOp (Cc n) = Cc (idOp n)
Now, I'm sure many of you are wondering why I didn't just write:

instance IdOp a a where
    idOp = id

I'll get back to that. Now, if I go zero steps, how hard is it to go
zero or one steps?
...
class ZeroOneStep a b where
    step :: a -> b
instance ZeroOneStep (Chain (At l)) (Chain l) where
    step (Ac n) = n
instance ZeroOneStep (Chain (Bt l)) (Chain l) where
    step (Bc n) = n
instance ZeroOneStep (Chain (Ct l)) (Chain l) where
    step (Cc n) = n
instance (IdOp (Chain l) (Chain r)) =>
    ZeroOneStep (Chain l) (Chain r) where
    step = idOp
That's quite nifty. I now need the allow-overlapping-instances, but it
works fine:
...
fooZeroOne :: (ZeroOneStep a b) => a -> b -> Bool
fooZeroOne _ _ = True
$ Main> fooZeroOne (Ac $ Bc Endc) (Ac $ Bc Endc)
$ True
$ Main> fooZeroOne (Ac $ Bc Endc) (Bc Endc)
$ True
$ Main> fooZeroOne (Ac $ Bc Endc) (Endc)
$ ...big exposion...
$ Main> fooZeroOne (Endc) (Bc Endc)
$ ...big exposion...
$ Main> fooZeroOne (Endc) (Endc)
$ True

So now I want zero or more steps, i.e. the Kleene *:
...
class ZeroMoreSteps a b where
    stepN :: a -> b
instance (ZeroMoreSteps (Chain l) (Chain r)) =>
    ZeroMoreSteps (Chain (At l)) (Chain r) where
    stepN (Ac n) = stepN n
instance (ZeroMoreSteps (Chain l) (Chain r)) =>
    ZeroMoreSteps (Chain (Bt l)) (Chain r) where
    stepN (Bc n) = stepN n
instance (ZeroMoreSteps (Chain l) (Chain r)) =>
    ZeroMoreSteps (Chain (Ct l)) (Chain r) where
    stepN (Cc n) = stepN n
I.e. if we can already get from l to r then it's not very hard to go
one step further. Now I need to bring in single step case:
...
instance (ZeroOneStep (Chain l) (Chain r)) =>
    ZeroMoreSteps (Chain l) (Chain r) where
    stepN = step
So now it should be done right? Because ZeroOneStep allows for zero
steps (via IdOp) so that should be it right?
...
fooZeroMore :: (ZeroMoreSteps a b) => a -> b -> Bool
fooZeroMore _ _ = True
$ Main > fooZeroMore Endc Endc
$ True
$ Main > fooZeroMore (Ac Endc) Endc
$ True
$ Main > fooZeroMore (Ac Endc) (Ac Endc)
$ ...big exposion...

Now what I think is happening is this: the rules for overlapping
instances say that the instance which is chosen is the one that
specifies the most information matching the particular context. In
this case, I think it's choosing and trying to use the "wrong"
instances because of this rule. Even if I try:
...
instance ZeroMoreSteps (Chain l) (Chain l) where
    stepN = id
It still blows up. So I have to do it really manually:
...
instance ZeroMoreSteps (Chain Endt) (Chain Endt) where
    stepN = id
instance ZeroMoreSteps (Chain (At l)) (Chain (At l)) where
    stepN = id
instance ZeroMoreSteps (Chain (Bt l)) (Chain (Bt l)) where
    stepN = id
instance ZeroMoreSteps (Chain (Ct l)) (Chain (Ct l)) where
    stepN = id
$ Main > fooZeroMore (Ac Endc) (Ac Endc)
$ True

Now it works. So am I right - is the reason for this the selection of
the instance to use given overlapping instances? If so, can anything
be done to make it "better"? I can think of two ideas, which I suspect
should both be laughed out of town asap: i) backtrack - if you can't
make the instance work then go back to where you last had a choice and
try the next instance; ii) whilst selecting the instance which is most
specific seems like the "sensible" choice, there are cases, eg guards,
where the vertical order in the program determines the ordering of
things to try. Maybe allow the programmer to specify an order to try
things in?

Note however how cool this now is:
...
data Cell :: * -> * where
             Cell :: x -> Cell a -- muh ha Ha HAA!
data Section :: * -> * -> * where
                SectionTo :: (ZeroMoreSteps a b) =>
                             (Cell a) -> b -> Section a b
                SectionFrom :: (ZeroMoreSteps a b) =>
                               a -> (Cell b) -> Section a b
fooCoolness :: (ZeroMoreSteps a b) =>
               a -> Section a b -> Section a b -> b
fooCoolness chain _ _ = stepN chain
$ Main > fooCoolness (Bc . Ac $ Endc)
                     (SectionTo (Cell True) (Ac $ Endc))
                     (SectionFrom (Bc . Ac $ Endc) (Cell 1))
$ Ac ~> Endc

And stepN just goes the "right" number of steps. The point is that I
don't need to use pattern matching to decompose the various
constructorsof Section in order to find (and perhaps fail) the unused
section of the chain.

Cheers,

Matthew

[Haskell-cafe] Kleene star in types

Matthew Sackman