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  4056 reads

Browse archivesActive forum topics 
Recent comments
9 hours 13 min ago
9 hours 50 min ago
11 hours 8 min ago
11 hours 21 min ago
15 hours 30 min ago
16 hours 16 min ago
16 hours 16 min ago
22 hours 29 min ago
22 hours 51 min ago
23 hours 11 min ago