[Prev][Next][Index][Thread]
Further to V.Pratt's reply
Date: Tue, 28 Mar 89 11:57:19 BST
> From: Gavin Wraith <gavinw%cogs.sussex.ac.uk@nss.cs.ucl.ac.uk>
> ...
> 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