The Hope+C existential type is not unsound. With some help from Evan I
decoded your Haskell example, please excuse the reply being in Hope+C
:-)
Heterogenous list of windows in Hope+C (examples here are actually
Massey Hope+C, Hope+C is a moving target - but the type system is as
in Hope+C).
data Win == Win(alpha); ! useless, but is only an example !
type WinList == list(Win);
Index function:
let index : WinList # int -> Win == fun
(nil, _) <= error(...)
| (h::_, 1) <= h
| (_::t, n) <= index(t, n-1)
end;
so the two applications:
Index(wl, 1) & Index(wl, 2)
have the same type, but that is correct as the existential types
havn't been unpacked. However:
let same : Win # Win -> truval == fun
(Win(a), Win(b)) <= a == b
end;
is INCORRECT as the type of a & b are DIFFERENT - each seperate unpack
introduces a new unique type constant. The removal of Mitchell
restriction on the "escaping" of unpackaged values is fine; as each
one has a DIFFERENT unique type.
[Note: Hope+C is not totally sound - but this is not due to the type
system itself but rather to the existance of the unsafe (and
untypeable) polymorphic equality function (alpha # alpha -> truval).
As in many (most?) functional languages this function is a bit-level
compare... you can apply it to functions... infinite objects and get
true... It should really be removed, but everybody likes it! The
auto-generation of equality functions as in Haskell solves some of the
problems (type unsoundnes) and not others (equality of user-defined
abstract data types where structural equality is not correct), but is
a step in the right direction.]
Cheers,
Nigel
---
Dr Nigel Perry Email: [EMAIL PROTECTED]
Department of Computer Science Tel: +64 6 356 9099 ext 8900
Massey University Fax: +64 6 350 5611
Palmerston North
New Zealand
