Juan Carlos Arevalo Baeza wrote (on 28-05-01 18:02 -0700):
Just a very naive question, because I'm really curious. I've seen in previous messages here discussions about type systems using this kind of notation:
G |- f :: all x::S . T G |- s :: S -------------------------------------- G |- f s :: [s/x]T
I'd never seen it before, and a few searches I've launched over the net have turned up just a couple more examples of this notation, but without a single reference to how it works or what it means, or even what it's called, for that matter.
I'd appreciate any pointers.
May I also recommend my PL theory references page?: http://www.cs.uu.nl/people/franka/ref.html BTW, here is the quick version: It says: Suppose term f has type all x::S.T in free variable environment G. Suppose further that term s has type S in environment G. Then the term f s has type [s/x]T (T with s substituted for x) in environment G. But this in itself is really not very meaningful unless you assume some standard definitions. For example, there should be rules for introducing variables, introducing/eliminating "all" types, manipulating environments, a definition for substitution, etc. -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379