Re: [Haskell-cafe] Compose

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 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