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. Salutaciones, JCAB --------------------------------------------------------------------- Juan Carlos "JCAB" Arevalo Baeza | http://www.roningames.com Senior Technology programmer | mailto:jcab@roningames.com Ronin Entertainment | ICQ: 10913692 (my opinions are only mine) JCAB's Rumblings: http://www.metro.net/jcab/Rumblings/html/index.html
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
At 09:24 PM 5/28/2001 -0400, Mark Carroll wrote:
G |- f :: all x::S . T G |- s :: S -------------------------------------- G |- f s :: [s/x]T
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:
:) Thanx.
"I bet ...", "My impression of it is rather like ...", "..., but clearly that's not quite right or ...", "... might be ...", "... means, probably, ..."
I hope that's a start.
Ufff... O:-) Sorry for pointing this out, but I couldn't resist. No offense intended. I actually appreciate your response. Really, I mean it. But it's not quite what I was looking for O:-) Anyway, I just saw that I had another reply (this on direct email, not posted to the list) with more info, so if you (or anyone) wants it just ask. Anyway, as the helpful person said about the expression above, "It's a theorem, really". Any more takers? I still don't have any pointers to literature where this theorem notation is explained more fully, and I'd really like to have some. Salutaciones, JCAB --------------------------------------------------------------------- Juan Carlos "JCAB" Arevalo Baeza | http://www.roningames.com Senior Technology programmer | mailto:jcab@roningames.com Ronin Entertainment | ICQ: 10913692 (my opinions are only mine) JCAB's Rumblings: http://www.metro.net/jcab/Rumblings/html/index.html
----- Original Message ----- From: "Juan Carlos Arevalo Baeza" <jcab@roningames.com> To: <haskell@haskell.org> Sent: Tuesday, May 29, 2001 11:02 AM Subject: Notation question
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 think I've seen it (or something similar) in an imperative language called "Imp".
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
participants (4)
-
David Scarlett -
Frank Atanassow -
Juan Carlos Arevalo Baeza -
Mark Carroll