On Mon, 28 May 2001, Juan Carlos Arevalo Baeza wrote:
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.
(snip) I'm far from the right person to have a go, but while we're waiting for someone who knows what they're talking about: I bet that |- is 'entails'. My impression of it is rather like 'implies', but clearly that's not quite right or we wouldn't need a different term for it. The . might be 'such that'. The thing below the ----- might be a consequence of the two things above it. The [s/x]T means, probably, "T with s substituted for any occurrence of x". (Did I get that the right way around?) I hope that's a start. -- Mark