> > > 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
