[tel]

Your idea about `maybe (int (>= 0, <= 10))` is exactly correct, but there's an important point to emphasize around it:

In a DT language when you express such a type the compiler will demand that you write a type like maybe which can fail at runtime and demand that you handle that failure.

To the compiler, `int` and `int (>= 0, <256)` are different types which require an explicit conversion (though the particular choice of conversion may be implicitly defined, viz. Idris' Coerce typeclass). In order to do multiplication like you suggested you would have to provide enough information to the compiler (either at compile time via constants or via a possibly failing mechanism which generates proof requirements at runtime) that your multiplication will not violate the constraints of the type.

To you final point about tracking constraints, even those defined implicitly, I think the answer is no-ish. Most frequently, DT languages have such a richness of types that there's no way to infer them—you're forced to write out all of the top-level types. But the idea of passing around constraints like you're suggesting here is not impossible.

You might imagine a pair type like (in no particular notation)

    (x, x => [Constraint])

where the first is a number and the second indicates a type-level function taking that particular number to a set of proofs that certain constraints are satisfied. We could indicate all of this at the type level and demand the compiler ensure that constraints are not violated (i.e. we end up coercing between constrained types like this and some coercions, those that coerce to supersets of the current constraints, are valid only) and we could also define a loose kind of (+), (*), (-) etc on this pair type such that the result passes along the proper constraints.

[vilhelm_s]

Agreed in general, but it is possible to enable this style of constraint propagation by being restrictive about what kind of contraints you can write. In particular, the "LIQUID" family of languanges that have been developed at UCSD allows properties which are conjunctions of LInear IneQUlites, and can infer them automatically. The programmer would annotate one declaration of a variable with a constraint like (0 <= x < 10), and the system tries to infer suitable constraints for all other variables (calling out to an SMT solver, and using invariant inference techniques from the program analysis community).

Their latest research language is "Liquid Haskell", I think it could deal with jarrett's example out of the box (with the caveat that yes, you still need to write the test explicitly). They used to have an online demo where you could just type programs into a web form, but that doesn't seem to work right now...

[wging]

http://goto.ucsd.edu:8090/index.html ?

[vilhelm_s]

Thanks!

[tel]

Yeah, less power means greater inference. You can model liquid types in a DT language I believe, but you'll never have the same convenience.

[vilhelm_s]

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

[tel]

Yes, that's true—I lapsed in terminology. Maybe calling it ITT would be better? There's a lot of ambiguity there, of course. And less marketing.