User loginNavigation 
Constraint based hybrid typing and the Curry Howard IsomorphismI'm working on a constraint based hybrid type system. The idea is to use a constraint as the type of all the value that it could be bound to. For example a finite domain range constraint like 1..7 would be the type of integers between 1 and 7. By default this test would be done at runtime, but as there are some fairly strong ties between type inference and checking, and constraint propagation I think that it should be posible to move a lot of the checking to compile time. But the problem is that 1..7 would not ony have integers as members but also other ranges like 2..4, and most importantly, it would be a member of it self. Actually as any value could be considerd as a constraint, every term vould be a type (and a kind) and a member of itself. This would wreck havoc on the Curry Howard Isomorphism, as every proposition would be a prof of itself, and thats a rather meaningless logic language. But im not that good at type theory so I wonder exactly what do I lose by not being able to use CHI and other type theoretical works based on it? By Felicia Li Svilling at 20061019 04:59  LtU Forum  previous forum topic  next forum topic  other blogs  6769 reads

Browse archivesActive forum topics 
Recent comments
8 weeks 3 days ago
8 weeks 5 days ago
8 weeks 6 days ago
15 weeks 6 days ago
21 weeks 4 days ago
21 weeks 5 days ago
22 weeks 4 days ago
25 weeks 2 days ago
26 weeks 5 days ago
26 weeks 6 days ago