Home » forums » LtU Forum

Small Value Set Types

I want to use a kind of dependent type, which I am calling a small value set (SVS) for the time being. An SVS type is a finite set of values of a given type, and is a subtype of that type. One usage of the SVS type is for performing optimization passes (full and partial computations of constant expressions).

Using the concatenative language Cat as an example, given the following function f: 

define f { 30 12 + }

The inferred type is 

() -> (42)

Which means it consumes no values from the stack, and produces a single value of the simple dependent type 42.

Given the function g:

define g { [42] [13] if }

The inferred type would be:

(bool) -> (42|13)

Which means that the function consumes a single boolean value from the stack and produces a value of the SVS type containing the values 42 and 13. In other words the union of the simple dependent types 42 and 13.

Am I just renaming something else here?

By cdiggins at 2006-09-03 19:28 | LtU Forum | previous forum topic | next forum topic | other blogs | 6308 reads

Comment viewing options

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

Finite set types

See http://lambda-the-ultimate.org/classic/message6641.html for a link to a language with a type system that tackles some of these concepts very generally.

By Tim Sweeney at Sun, 2006-09-03 23:06 | login or register to post comments

The link was broken but I

The link was broken but I managed to track-down the Ontic language spec at http://ttic.uchicago.edu/~dmcallester/ontic-spec.ps

By cdiggins at Mon, 2006-09-04 00:16 | login or register to post comments

Can finite set types be used for static contract verification?

I wonder if finite set types/depentent types can be used for static contract verification. Does anyone think it is possible?

By Achilleas Margaritis at Mon, 2006-09-04 15:28 | login or register to post comments

Yes...

Yes... I thought that was the whole point of them? Have I been reading everything with a huge misunderstanding?

By genneth at Mon, 2006-09-04 16:28 | login or register to post comments

But what about recursive algorithms?

What about recursive algorithms? I think it is only possible to statically prove a subset of contracts, because proving all would contradict the halting problem. Is that a valid separation, and if so, has there been a formal paper that separates contracts into statically provable and non-provable?

By Achilleas Margaritis at Tue, 2006-09-05 15:06 | login or register to post comments

Decidability

What about recursive algorithms? I think it is only possible to statically prove a subset of contracts, because proving all would contradict the halting problem.

Yes, type-checking in a dependently-typed language is undecidable, i.e. at least as hard as the halting problem.

Is that a valid separation, and if so, has there been a formal paper that separates contracts into statically provable and non-provable?

It's a valid separation but I'm not sure what exactly you're expecting of such a paper. By its very nature you are not going to see an effective classification ("effective" in Turing's sense) of checkable and non-checkable dependent type declarations that doesn't have either false positives or false negatives. If you're asking for a characterization of a useful and expressive subset of checkable types then you can take a look at the various type systems with a decidable type-checking algorithm, i.e. the majority of type systems discussed here. For instance, type-checking in vanilla System F is undecidable but there are expressive and only slightly weaker variants that admit decidable type-checking. The Curry-Howard isomorphism is essential for understanding the relationship between type systems and the propositional contracts they can express. For instance, it would tell you that System F corresponds to a second-order logic.

By Per Vognsen at Tue, 2006-09-05 17:09 | login or register to post comments

Yes, type-checking in a

Yes, type-checking in a dependently-typed language is undecidable, i.e. at least as hard as the halting problem.

This isn't necessarily true - the language may be strongly normalising, or might insist that its types are by only allowing them to depend on a subset of terms.

Also, type-checking in a Church-style System F (that is, with explicit type annotations) is decidable, it's a Curry-style one that's undecidable - I imagine most of us think of the Church-style version when we read "vanilla System F", as type-checking a Curry-style calculus is not far removed from type inference.

By Philippa Cowderoy at Tue, 2006-09-05 18:20 | login or register to post comments

Corrections

Yes, type-checking in a dependently-typed language is undecidable

That's not true. For example, type checking in the calculus of constructions - one canonical dependently typed lambda calculus - is decidable, because it is terminating. This holds for a number of other systems as well.

type-checking in vanilla System F is undecidable

That's not true either. Type checking System F (a subsystem of the calculus of constructions) is perfectly decidable. What is not decidable is type inference for System F.

Programming languages like ML form significant subsets of System F (F_omega, in fact), for which even type inference is decidable.

By Andreas Rossberg at Wed, 2006-09-06 01:00 | login or register to post comments

Thanks

I clearly wasn't very careful or precise. Thanks for the corrections.

By Per Vognsen at Wed, 2006-09-06 02:05 | login or register to post comments