Notation question

[Frank Atanassow]

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