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