Further to V.Pratt's reply

Date: Tue, 28 Mar 89 11:57:19 BST

>       From: Gavin Wraith 
> <gavinw%cogs.sussex.ac.uk-LEftKC8aXbilgWnZye4G+Q@xxxxxxxxxxxxxxxx>
>       ...
>        What I ought to have said is that values of a recursive sum
>        (initial algebra) A(T) are well-founded over T (can be
>        expressed as a term involving constructors and T-values)
>        whereas values of a recursive product (final coalgebra) B(T)
>        are not in general.
>
> Is strictness still meant to fit in here?

  No - this is a remark about values rather than about evaluation.


>        We would expect quite different representations for values of
>        type (U+V)*W from representations of values of type
>        (U*W)+(V*W).
>
> This would seem to contradict both theory and practice:  if two objects
> are isomorphic then surely the same representation can serve for both.

Here I disagree. Consider the ML definitions

datatype ('a,'b) sum = inl of 'a | inr of 'b ;

datatype ('u,'v,'w) distribute_1 = sumfirst of (('u,'v) sum)*'w ;

datatype ('u,'v,'w) distribute_2 = sumlast of ('u*'w,'v*'w) sum ;

with

fun f (sumfirst ((inl x),z)) = sumlast (inl (x,z))
  | f (sumfirst ((inr y),z)) = sumlast (inr (y,z)) ;

fun g (sumlast (inl (x,z))) = sumfirst ((inl x),z)
  | g (sumlast (inr (y,z))) = sumfirst ((inr y),z) ;

Then of course f is an isomorphic function of type

       ('a,'b,'c) distribute_1 -> ('a,'b,'c) distribute_2

with inverse g, but the type checker cannot "know" this, and I doubt
whether any implementation of ML would ever represent the type
constructors distribute_1 and distribute_2 in the same way !
It comes down to this business of only being able to cope adequately
with free systems; equations mean word problems. I would not want to
decide on some arbitrary canonical forms for types. On the other hand
I think it would be quite reasonable to ask of a type system that
it would compile automatically the isomorphisms f and g, because they
are natural isomorphisms between distribute_1 and distribute_2 in a
very strong sense.

Gavin Wraith