[CST-2] Types (NOT Opt Comp.) 1997/7/10

[Sam Staton]

> Well the language he gives doesn't seem to have type schemes.
Well, but it has type variables.

We might make a rule

G |- M : t     G |- t > t'
----------------------------
G |- M : t'

Where '>' is some generalises relation like that used on slide 24:

 'a,G |- 'a > int
 'a,G |- 'a > bool
 'a,G |- 'a > (t -> t')
 'a,G |- ('a -> t) > (t' -> t)

etc.

Then (using \ for lambda)

'a,G |- \x.x : 'a -> 'a

(if/how you introduce type variables is another question!)

and, by the above rule

'a,G |- \x.x : int -> int

since 'a,G |- ('a -> 'a) > (int -> int)

In keeping with the definition of principle type scheme on slide 24, say
that the principle type of M is the most general type that it can have.

In this case, the principle type of \x.x is 'a -> 'a.

Sorry, the ascii looks a bit confusing, but it should make sense.

-- 
sam

On Fri, 24 May 2002, Matej Pfajfar wrote:

> Well the language he gives doesn't seem to have type schemes.
> So the rules & axioms of the type system don't exhibit the principal
> type property.
>
> Is that plausible?
>
> On Fri, 24 May 2002, Alvin wrote:
>
> > Hmm, maybe it just means whether generalisation is possible.  Eg the tuple
> > rule:
> >
> > G |- M1 : t1    G |- M2 : t2
> > -----------------------------
> >     G |- (M1,M2) : t1 x t2
> >
> > Is a generalised form of
> >
> > G |- M1 : r     G |- M2 : r
> > ---------------------------
> >     G |- (M1,M2) : r x r
> >
> > Similarly for integers, functions etc
> >
> > Total guess, but it makes sense.
> >
> > Alvin
> >
> > > Sorry I just realised the mistake. The question (repeated below) is
> > > clearly about Types, not Opt. Comp.
> > >
> > > Mat
> > >
> > >> The question asks to explain the notion of a principal type. Presumably
> > >> the answer to this is that the principle type is just the principal type
> > >> scheme.
> > >> Then it also asks whether the set of type inference rules (for an ML-like
> > >> language), which you had to give in the previous part of the question, has
> > >> this propery.
> > >> I am a bit confused as to how type inference rules exhibit a principal
> > >> type property? Anyone?
> > >> thanks,
> > >>
> > >> Mat
> > >>
> > >> Matej Pfajfar
> > >> St John's College, University of Cambridge, UK
> > >>
> > >> GPG Public Key @ http://matejpfajfar.co.uk/keys
> > >> Most people are good people, the rest of us are going to
> > >> run the world. -- badbytes
> > >>
> > >> WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
> > >>          30/09/2002. PLEASE USE mp@cantab.net.
> > >>
> > >>
> > >>
> > >> _______________________________________________
> > >> CST-2 mailing list
> > >> CST-2@srcf.ucam.org
> > >> http://www.srcf.ucam.org/mailman/listinfo/cst-2
> > >>
> > >
> > > Matej Pfajfar
> > > St John's College, University of Cambridge, UK
> > >
> > > GPG Public Key @ http://matejpfajfar.co.uk/keys
> > > Most people are good people, the rest of us are going to
> > > run the world. -- badbytes
> > >
> > > WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
> > >        30/09/2002. PLEASE USE mp@cantab.net.
> > >
> > >
> > >
> > > _______________________________________________
> > > CST-2 mailing list
> > > CST-2@srcf.ucam.org
> > > http://www.srcf.ucam.org/mailman/listinfo/cst-2
> >
> >
> >
> > _______________________________________________
> > CST-2 mailing list
> > CST-2@srcf.ucam.org
> > http://www.srcf.ucam.org/mailman/listinfo/cst-2
> >
>
> Matej Pfajfar
> St John's College, University of Cambridge, UK
>
> GPG Public Key @ http://matejpfajfar.co.uk/keys
> Most people are good people, the rest of us are going to
> run the world. -- badbytes
>
> WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON
>          30/09/2002. PLEASE USE mp@cantab.net.
>
>
>
> _______________________________________________
> CST-2 mailing list
> CST-2@srcf.ucam.org
> http://www.srcf.ucam.org/mailman/listinfo/cst-2
>