Question

Say I have Simply typed lambda calculus, and add an assignment rule:

<identifier> : <type> = <abstraction>

Where <identifier> is the name of the function, <type> is the function type and <abstraction> is the abstraction to be assigned to the identifier.

Then I add a typing rule that says that when you see an assignment such as the above, you use a temporary type context, in which the declared type (the one in <identifier> : <type>) is associated with the identifier, to type check <abstraction> and then make sure the declared type equals the abstraction's type.

And finally I add another rule that would let me have a list of assignments on top of a lambda term which is the one I'd evaluate, such that all these assignments would be added to the global scope before the term is evaluated.

Seems to me that this alone would make it Turing complete since I'd be able to do stuff like:

stackoverflow: NUM -> NUM = λn:NUM.(stackoverflow n)
(stackoverflow 0)

And at the same time, everything I can define in this language would be "well typed" in the sense that it wouldn't be able to define infinite types (I wouldn't be able to define the Y combinator).

So my questions are, is this really Turing complete? And, am I missing something when I say everything would be "well typed" (like for instance, I could define the Y combinator in a way I haven't yet realized or is there any gotcha in this type system)?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top