[Haskell-cafe] Compose

[Conor McBride]

Hi folks

(For those of you at ICFP, my best regards and humblest apologies! I
have unavoidable and troublesome distractions which keep me within
the UK, but at quite a high average speed.)

On 30 Sep 2007, at 15:58, Felipe Almeida Lessa wrote:

> On 9/30/07, PR Stanley <prstanley at ntlworld.com> wrote:
>> So the question is, does compose as a function or keyword exist in
>> Haskell and if so how can the above code frag be corrected?
>> O and, is compose in any way related to curry and uncurry?
>
> You can't write that function in Haskell as the list is heterogeneous.

It's not so easy in Haskell 98 (but I know better than to be confident
about its impossibility). It's not a problem with GADTs, however. [Rant
about gratuitous renaming and revisionist history deleted.]

 > data Star f s t where
 >   Nil :: Star f r r
 >   (:*) :: f r s -> Star f s t -> Star f r t

 > squish :: (forall r. f r r) -> (forall r s t . f r s -> f s t -> f  
r t) ->
 >           Star f s t -> f s t
 > squish i c Nil = i
 > squish i c (rs :* st) = c rs (squish i c st)

 > type Composition = Star (->)

 > compose :: Composition s t -> s -> t
 > compose = squish id (flip (.))

Next, the inevitable digression.

As dependently typed programmers are beginning to discover, Star is the
new []. A bunch of our favourite structures are stellar, from natural
numbers and lists...

 > data NatStep s t where
 >   Suc :: NatStep () ()

 > type Nat = Star NatStep () ()

 > data ListStep a s t where
 >   Cons :: a -> ListStep a () ()

 > type List a = Star (ListStep a) () ()

...to vectors and finite sets.

 > data SUC a = SUC a
 > data ZERO = ZERO

 > data VecStep a s t where
 >   VCons :: a -> VecStep a (SUC n) n

 > type Vector n a = Star (VecStep a) n ZERO

 > data LO = LO
 > data HI = HI

 > data FinStep s t where
 >   Now :: FinStep (SUC n, LO) (ZERO, HI)
 >   Later :: FinStep (SUC n, LO) (n, LO)

 > type Fin n = Star FinStep (n, LO) (ZERO, HI)

In fact, a vector can be seen as a "natural number with labelled edges"
whilst a finite set element is a "natural number with a selected edge".
When you have genuine dependent types, you can express these labelling
and selection patterns once and for all, indexing one instance of Star
(Vector, say) by data drawn from another such instance (Nat, say).

If you're interested, you can find a generous lump of Agda 2 code
devoted to investigating these phenomena here:

   http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/AIM6/Path/

(The code was hacked up earlier this year at the 6th Agda Implementors'
Meeting, mostly by Ulf Norell, with a little provocation from me.)

It was a real penny-drop moment for us: we coded up a general sequence
structure which was parametric in the index discipline, giving a uniform
presentation to lists-with-diverse-extra-weirdness. The reusability
absolutely relies on indexing datatypes by ordinary data, rather than
some type-level analogue. One should bear in mind such examples (amongst
others, no doubt) if one is planning to claim that GADTs + this or that
= dependent programming.

All the best

Conor