> > > 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
John Hughes said
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!
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. I seem to spend half my life using such inductive definitions and the other half teaching them to undergraduates (and the third half doing university administration, hey ho). Casting modesty aside, to read about such things let me recommend <www.cl.cam.ac.uk/Teaching/2000/Semantics/> lecture notes on operational semantics (esp section 2.3) Andy Pitts
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
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
participants (4)
-
Andrew Pitts -
John Hughes -
Jon Fairbairn -
Tom Moertel