Constraint based hybrid typing and the Curry Howard Isomorphism

I'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?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What are you trying to gain?

If we flip your question around, and consider what you are trying to gain by means of your type system, we might get a more interesting answer.

The essence of Curry-Howard is that you start with a system (untyped LC) that over-generates: it contains a bunch of non-normalizing terms. By imposing a restriction expressed as a type system, you eliminate the possibilities that you don't want.

If the type system you impose isn't equivalent to a sensible logic of some kind or another, it likely isn't going to eliminate a sensible class of possibilities.

(The original CH works because it so happens that being able to find a constructive proof in intuisionistic logic is exactly the problem of find a normal form for an LC term.)

So ask yourself: what kinds of programs am I trying to eliminate? How can I describe those using a logic? And then use that logic for your type system.

Otherwise, what is the point of the type system in the first place?

I'm not sure I buy your

I'm not sure I buy your phrasing - how do I describe non-termination using a logic? It seems to me that what's interesting is what we include.

An instance of an Intuitionist

how do I describe non-termination using a logic? It seems to me that what's interesting is what we include.

I see that you don't accept the law of the excluded middle: an excellent demonstration of intuistionistic logic. ;-)

If you prefer, you could conceive of it the other way around: I want to select the class of only and all the normalizing terms in untyped LC, observe that those are equivalent to those that can be proven in intuisitionistic logic, and use that.

I just think this requires a bigger leap of discovery than the other way around in this instance.

Put differently, how do you define the universe of possibilties of what you might include a priori? Isn't it easier to start from something too much and whittle it down to just right?

It depends on the things

It depends on the things you're looking to exclude. We already know from conventional logic that if we wish to exclude non-termination we're going to have to throw away some terminating terms as well. I don't know if that's been shown to apply to the functions described as well as the terms (though I suspect so), I should go poke around the big pile of CS theory results again.

Now there's a thought: is there an intuitionistic proof that the halting problem's only semi-decidable (I'll settle for proving it's not decidable)?

Certainly ideas like the lambda cube and extending typing to subtyping seem to me to show a progression of things we can include - as do advances like qualified types.

Edited to add: Of course, substructural types would be an option in the other direction, and qualified types are only an improvement if you're not willing to let your polymorphism be unsound!

The mountains are mountains, the rivers are rivers

Sheesh, it's hard to answer a simple question with a simple answer around here. ;-)

Li's original question probably doesn't involve non-termination; it just so happens that part of the interesting correspondence in CH involves strong normalization.

If you want to generalize the notion of types as logical constraints on the well-formedness of programs (which seems to be Li's intent), I'm suggesting using this "what do you want to filter out" approach as a way of thinking about it.

Obviously, there is lots more to say about CH, types and programming, intuitionistic logic, etc. I'm just trying to spread it out over a longer period by addressing one problem at a time. ;-)

What I am trying to gain.

The point is to localize errors. To make exact descriptions of the domain of functions so that as many logical errors as possible also are type errors. And to make sure that they are detected as soon as possible.

I am not focusing on type inference or actually eliminating any specific class of programs. Just to make sure that if the program breaks its specification, its reported as soon as possible.

In which case you're left

In which case you're left looking at rendering the specification as a type - which in many ways throws you right in the deep end because you need a decently powerful logic.

Yes I have that, the thing

Yes I have that, the thing Im worried about is that the logic is to powerful.

Stand on the shoulders of giants

If you are wobbly on all the gory details about the power and limitations of type systems and logical systems, maybe the thing to do is look at specific examples that have already been developed by others to deal with such problems.

The example you originally gave about delimited ranges has been looked at by the dependent-typing folks (the much-discussed-here Epigram, for example.) What the trade-offs, limitations and problems of such regimes are already much thought about and described.

If someone had already developed the perfect type system that had all the right power and none of the short-comings. type theory would no longer hold much interest. Given that it is still a hard problem, standing on the shoulders of giants rather than trying to do your own from scratch is probably the way to go.