[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Conor McBride]

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