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'd appreciate any pointers. Salutaciones, JCAB - Juan Carlos "JCAB" Arevalo Baeza| http://www.roningames.com Senior Technology programmer| mailto:[EMAIL PROTECTED] Ronin Entertainment | ICQ: 10913692 (my opinions are only mine) JCAB's Rumblings: http://www.metro.net/jcab/Rumblings/html/index.html ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
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:[EMAIL PROTECTED] Ronin Entertainment | ICQ: 10913692 (my opinions are only mine) JCAB's Rumblings: http://www.metro.net/jcab/Rumblings/html/index.html ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
- Original Message - From: "Juan Carlos Arevalo Baeza" <[EMAIL PROTECTED]> To: <[EMAIL PROTECTED]> 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". ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
> > > G |- f :: all x::S . T G |- s :: S > > >-- > > > G |- f s :: [s/x]T > 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. This is a standard notation for describing type systems in articles on the subject -- so standard that it's hard to think of a good reference that actually explains it! However, I'd suggest looking at Michael Schwartzbach's lecture notes on Polymorphic Type Inference, which are on the web at http://www.daimi.aau.dk/~mis/typeinf.ps The typing rule notation is explained in the first couple of pages, and then used to explain many variants on type systems, show how inference works, etc. I have a collection of links to such articles at http://www.md.chalmers.se/~rjmh/tutorials.html which you might find useful. John Hughes ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
> and not just type systems but also other aspects of operational > semantics. What we have here is a single rule from a rule-based > inductive definition of a certain relation G |- s :: S between typing > environments G, expressions s and types S. It's probably worth mentioning here that this notation originated (I think) in mathematical logic, as a way of presenting formal systems. Try "Gentzen", "Natural Deduction" and "Sequent Calculus" as search terms. Jón ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Notation question
Another introduction, with emphasis on the historical development: Philip Wadler, "Proofs are Programs: 19th Century Logic and 21st Century Computing." http://www.cs.bell-labs.com/who/wadler/topics/history.html It's a fun read, too. Cheers, Tom ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
