> I've lost track of what we're talking about here. In what system can
> we not hope for principal types? (I believe that there are type
> theories with dependent types, such as the one in Thompson's _Type
> Theory and Functional Programming_, where each term has at most one
> type; so it can't just be dependent types that disallow principal
> types.)
Well, maybe there are, but Cayenne doesn't have that property.
Again, I think this is a feature, not a bug. I'll include
a small example below.
> Could you give an example? I can't think how to construct a
> Haskell 98 program with this property (unless you count "compiling"
> and "failing to compile" as different results).
Check the example I sent in reply to Fergus' request.
-- Lennart
struct
abstract
type Stack a = List a
push :: a -> Stack a -> Stack a
push x xs = x : xs
...
This has type
sig
type Stack a
push :: a -> Stack a -> Stack a
...
Outside the defining struct Stack is abstract and cannot be
interchanged for List.
But here's another type we could give push
push :: a -> List a -> Stack
which (outside the defining struct) would look like a totally
different creature.
