User loginNavigation 
ConstraintBased Type Inference for Guarded Algebraic Data Types
ConstraintBased Type Inference for Guarded Algebraic Data Types
Quite a mouthful, but look: Guarded algebraic data types, which subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and phantom types, and are closely related to inductive types, have the distinguishing feature that, when typechecking a function defined by cases, every branch must be checked under different typing assumptions. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information. I still have to grok this idea of "dynamic tests producing extra static type information" in its entirety, though. By Andris Birkmanis at 20040809 20:48  LtU Forum  previous forum topic  next forum topic  other blogs  6438 reads

Browse archives
Active forum topicsNew forum topics 
Recent comments
1 week 3 days ago
1 week 6 days ago
3 weeks 10 min ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 4 days ago
5 weeks 22 hours ago
5 weeks 22 hours ago
6 weeks 6 days ago
10 weeks 1 day ago