[Haskell-cafe] Kleene star in types

[Matthew Sackman]

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