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

Browse archives
Active forum topicsNew forum topics 
Recent comments
4 days 17 hours ago
2 weeks 2 days ago
2 weeks 5 days ago
3 weeks 6 days ago
4 weeks 2 days ago
4 weeks 3 days ago
4 weeks 3 days ago
6 weeks 11 hours ago
6 weeks 12 hours ago
7 weeks 5 days ago