Sun Mar 4 15:11:23 CET 2018

CCC pattern matching

How does this implement pattern matching?  For code similar to GW,
this is pretty much all there is: data structures to decouple modules,
with data moving all over the place.

A pattern match is a mating of a set of costructors and a set of
cases.  Compare to app / lam?

app :: r a -> r (a -> b) -> r b
lam :: (r a -> r b) -> r (a -> b)

Now suppose a is a sum type.  It is never explicitly represented as a
sum type in the meta language: all types are always wrapped.

I did this for sum types (tuples) before.  Just try Either with some
concrete base types.

Suppose we're interested in this function

f_w :: r (Either Int Float  -> Bool)
f_i :: (r (Either Int Float)) -> (r Bool)

The point of hiding this behind r, is that the representation is
completely opaque.  I.e. the "target compiler" needs to have a special
case to implement deconstruction.

In that sense, sums and products are indistinguishable.


r (a -> b)      Opaque representation of function.  Here a->b is just an index.
(r a) -> (r b)  Actual function mapping one rep to another.

What do app and lam create?  A way to use native function abstraction,
application to create representations of functions.

The point is to create reps of funcs.

Specialized to Ether: the point is to create a rep of e.g Erlang

  fun({left, X}) -> inc(X);
     ({right,Y}} -> dec(Y).

From a Haskell meta-language function:

  \e -> case e of
     Left x  -> app r_inc x
     Right y -> app r_dec y

r (Either A B -> C)
Either (r A) (r B) -> r C

For every target language type, there needs to be an operation that
lifts it out like this.  Sums or products really do not matter.

In this case, a specialized "appEither" is needed

appEither ::
r (Either A B) ->
r (Either A B -> C) ->
r C

but what about

(Either (r A) (r B) -> r C) 
-> r (Either A B -> C)

I'm confusing two things:
- function abstraction / application
- type construction / deconstruction

These are very similar, but they need to be implemented in a way that
they can be mixed.

A case statement takes two representations of functions, one for each

caseEither ::
r (Either A B)
-> r (A -> C)
-> r (B -> C)
-> r (Either A B -> C)

So, the solution is to implement "case" explicitly for each sum type.
Pattern matching is a _syntactic_ overlay for case, and should not be
modeled in the representation.

The counterpart is explicit constructor functions

EitherL :: r A -> r (Either A B)
EitherR :: r B -> r (Either A B)

Main point, per datatype:
- a case function
- constructors

However, generic 2-ary sum and product are enough to structurally
mimick any possible ADT.

So "ML" is:
- app/lam
- cons/uncons (products)
- either/uneither (sums)

Starting to recall how this was explained in the final tagless lit.