Conor McBride ctm at cs.nott.ac.uk
Tue Jan 4 05:23:13 EST 2005

```ajb at spamcop.net wrote:
> G'day all.
>
> Quoting Conor McBride <ctm at cs.nott.ac.uk>:
>
>
>>Where now? Well, counterexample fiends who want to provoke Oleg into
>>inventing a new recipe had better write down a higher-order example.
>>I just did, then deleted it. Discretion is the better part of valour.
>
>
> Thankfully, I'm the sort of person who doesn't know when to stop.
>
> Is this the sort of thing you had in mind?
>
> <<
> -- WARNING: This code is untested under GHC HEAD
>
> data State s a
>   = Bind :: State s a -> (a -> State s b) -> State s b
>   | Return :: a -> State s a
>   | Get :: State s s
>   | Put :: s -> State s ()

Well, it's certainly higher-order, and the polymorphism might be amusing.
Obviously the interesting thing is Bind.

The idea is to have a class GoodState e s a capturing the good guys. The
hard part is expressing that the Kleisli arrow always makes good.

-- boring bits
data State s a = forall e. GoodState e s a => State e
class GoodState e s a where {}

data Return a = Return a
instance GoodState (Return a) s a where {}

data Get = Get
instance GoodState Get s s where {}

data Put s = Put s
instance GoodState (Put s) s () where {}

-- now we've got work to do
{- tempting, but wrong (why?)
data Bind e f
instance (GoodState ea s a, GoodState eb s b) =>
GoodState (Bind ea (a -> eb)) s b
-}

-- this looks better
data Bind s a b = Bind (State s a) (a -> State s b)
instance GoodState (Bind s a b e) s b

Actually, that's a clue towards a better recipe...

The trouble with this example is that, although higher-order at
the data level, we don't need a higher-order constraint to
make the function produce goodness, because we can use a first-order
constraint in an existential type. That trick might get us a long
way.

The potential villains of the piece are
(i)  higher-order constraints  (GoodInput this => GoodOutput that)
(ii) polymorphic constraints---how does one abstract over, say,
numerically indexed families?

But thank you for that example because
(i)  it's a good example of an idiom of dependently typed
programming---turning combinators into constructors;
(exercise: why is parsing an application of the
remainder theorem?)
(ii) it has been suitably provocative, at least in my head

Cheers

Conor

--
http://www.cs.nott.ac.uk/~ctm
```