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

4 Jan 2005

      ajb@spamcop.net wrote:
...
G'day all.
Quoting Conor McBride :
...
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