Motivation for erase

Moderator: Type Systems of Programming Languages

Benutzeravatar
timo.b
Mausschubser
Mausschubser
Beiträge: 79
Registriert: 28. Sep 2009 16:18

Motivation for erase

Beitrag 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

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Motivation for erase

Beitrag 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.

Benutzeravatar
timo.b
Mausschubser
Mausschubser
Beiträge: 79
Registriert: 28. Sep 2009 16:18

Re: Motivation for erase

Beitrag 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.

Antworten

Zurück zu „Type Systems of Programming Languages“