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

Browse archivesActive forum topics 
Recent comments
2 days 17 hours ago
3 days 12 hours ago
3 days 16 hours ago
3 days 16 hours ago
3 days 18 hours ago
3 days 18 hours ago
3 days 19 hours ago
3 days 19 hours ago
3 days 23 hours ago
3 days 23 hours ago