## Assignment 5.1

Moderator: Type Systems of Programming Languages

daehn
Erstie
Beiträge: 16
Registriert: 5. Okt 2010 13:42

### Assignment 5.1

Heyho,

I just tried to do Task 1.2 and stumpled upon giving a "concrete" type for an example expression. IIRC for the "core" lambda calculus, there are only the types T ::= T -> T, but then how do i give a concrete type? (Do I miss some kind of "anchor"?)

Consider e.g.

Code: Alles auswählen

e = \x : ? . x
What do I put for "?". Is this possible at all or should we consider the expressions enriched with numerical expressions or such?

I think the problem might be rooted even deeper, as the book states (Excercise 9.2.1 and the Solution in the Appendix):
The pure simply typed lambda-calculus with no base types is actually degenerate, in the sense that it has no well-typed terms at all. [...] Because the set of type expressions is empty (there is no base case in the syntax of types).
Edit: Actually, the same question applies to Task 2.2.

erdweg
Moderator
Beiträge: 60
Registriert: 28. Mär 2013 10:08

### Re: Assignment 5.1

daehn hat geschrieben: I just tried to do Task 1.2 and stumpled upon giving a "concrete" type for an example expression. IIRC for the "core" lambda calculus, there are only the types T ::= T -> T, but then how do i give a concrete type? (Do I miss some kind of "anchor"?)

Consider e.g.

Code: Alles auswählen

e = \x : ? . x
What do I put for "?". Is this possible at all or should we consider the expressions enriched with numerical expressions or such?
Right. If you want to give a counter example, you need to add some base type, such as Num or Bool.

AlexanderF
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

### Re: Assignment 5.1

Ok,

but without base type the proof is trivial,

because there are no types,
therefore no expression is typable at all,
therefore the premise Gamma |- e' : T is wrong.