[CST-2] Types

[George van den Driessche]

The typing relation is over triples (Environment, Expression, Type). It's
the one that looks like

    Environment |- Expression : Type

You define it inductively by stating its rules and axiom.

G |- x : a    if Gok & {x:a} e Gta. (var)

G,{x:a} |- M : b
---------------- (fn)
G |- lx.M : a->b

G |- M1 : t1 -> t2    G |- M2 : t1
---------------------------------- (app)
    G |- M1 M2 : t2

G |- M : t1
------------------ (gen)
G |- /\a.M : Va.t1

G |- M : Va.t1
------------------ (spec)
G |- M b : t1[b/a]

(Plus a few side-conditions here and there.)


Does that help?

George

----- Original Message -----
From: "Alvin" <ah296@cam.ac.uk>
To: <cst-2@srcf.ucam.org>
Sent: Monday, May 06, 2002 12:54 AM
Subject: [CST-2] Types


> Brief question on types.
>
> 2001 Paper 9 Question 6
>
> Part a - define the typing relation of the polymorphic lambda calculus
> (PLC).
>
> Probably a stupid question, but what's the typing relation?!  And how does
> one define it?
>
> Alvin
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2