User loginNavigation 
What is a Type?After going through both of the Types and Programming Languages books, I am starting to feel confident in my understanding of Type Systems in terms of how they would be implemented. However, I still feel uncomfortable with the theoretical foundations; even after going through the proofs it still seems like a lot of handwaving when defining what is a type. So to try to find a good mental model of what a type is I thought I would ask LtU: what is a type? The reason for my uneasiness probably stems from my background programming in both static and dynamic type systems. The static definition of types seems to tend more towards what can be proven at compile time. This definition seems to put more emphasis on creating type systems which are strongly normalizing. However, in dynamic type systems, types are often manipulated as terms. Trying to find a consistent mental model for these two usages of the term (especially after the introduction of subtyping) I am currently stuck with defining them as propositions which map terms to truth values. The intuition is that a type is a proposition, nothing more. I can't seem to find much theory for such a model and that prompted this post. Is this highly inconsistent with current theory? More formally, what would your initial reaction be to a system where: Î»t:T.x â†’ Î»t. if T(t) then x else TypeError By andrew johnson at 20091027 23:30  LtU Forum  previous forum topic  next forum topic  other blogs  5778 reads

Browse archives
Active forum topics 
Recent comments
5 weeks 5 days ago
5 weeks 5 days ago
5 weeks 5 days ago
27 weeks 6 days ago
32 weeks 1 day ago
33 weeks 5 days ago
33 weeks 5 days ago
36 weeks 3 days ago
41 weeks 1 day ago
41 weeks 1 day ago