Seite 1 von 1

Motivation for erase

Verfasst: 6. Mär 2014 17:05
von timo.b
Hi,

in the lecture (19.11.) the function \(erase\) was introduced. This function takes an typed term and computes an untyped term. What is the motivation of using/writing the \(erase\)-function?

Thank you for an answer,
kind regards
Timo Bähr

Re: Motivation for erase

Verfasst: 6. Mär 2014 17:32
von dschneid
The motivation is basically to demonstrate that the types are only used by the type checker, and do not influence the execution of terms.

Re: Motivation for erase

Verfasst: 6. Mär 2014 19:06
von timo.b
dschneid hat geschrieben:The motivation is basically to demonstrate that the types are only used by the type checker, and do not influence the execution of terms.
Thank you. I asked me if there was more than that.