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 2006-10-19 04:59 | LtU Forum | previous forum topic | next forum topic | other blogs | 7449 reads
|
Browse archives
Active forum topics |
Recent comments
37 weeks 1 hour ago
37 weeks 4 hours ago
37 weeks 4 hours ago
1 year 7 weeks ago
1 year 11 weeks ago
1 year 12 weeks ago
1 year 12 weeks ago
1 year 15 weeks ago
1 year 20 weeks ago
1 year 20 weeks ago