[jarrett]

A thought on dependent types:

Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code):

  // Variable x is an integer greater than or equal to 0 and less than 256.
  int x (>=0, <256) 

  x = 128 // This is valid.
  x = x * 3 // This violates the type.

I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this:

  int x (>= 0, <=10)
  x = parseInt(getKeyboardInput)

Now the compiler can't know for sure whether the type has been violated, because the value of getKeyboardInput could be anything. To take a page from Haskell, you could do something like this (which is still pseudocode, not valid Haskell):

  // x is a value that is either 1) an int from 0 to 10, or 2) nothing at all.
  maybe (int (>= 0, <=10) x
  
  // applyConstraint recognizes that parseInt may return a value violating x's contraints.
  // Thus it transforms the return type of parseInt from int to maybe (int (>= 0, <=10)
  x = applyConstraint(parseInt(getKeyboardInput))

Or perhaps applyConstraint wouldn't have to be called explicitly, but would be implicitly added by the compiler as needed. I'm not sure which is better stylistically.

Either way, applyConstraint would be required any time a computation could return an invalid value. That would get tricky, because the compiler would have to track the constraints on every variable, even where those constraints aren't declared. For example:

  int w (>= 0, <= 10)
  int x (>= 0, <= 2)
  int y
  int z (>= 0, <= 20)

  y = w * x
  z = y

Here, the compiler would have to infer from the assignment "y = w * x" that y is always between 0 and 20.

Do any languages currently take the idea this far (or farther)?

[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.

[JoshTriplett]

The compiler doesn't necessarily have to have that level of inference; it can simply require the code to prove the constraints. For instance, parseInt will return an unconstrained int, so you'll get a type error trying to assign that to a range-constrained int. For your first and last examples, the multiplication operator on range-constrained ints can easily propagate the range constraints. In your last example, `z = w * x` would work, but assigning through the unconstrained int y may simply cause the last assignment z=y to produce a type error, forcing the code to re-establish the constraint explicitly.

[rybosome]

As others have noted, it's less about the compiler running code and making determinations as it is using extremely robust, information-rich types. For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector. Operations that increase the size of the vector are guaranteed to return a non-empty vector. They might look something like this:

    (::) : a -> Vector a n -> Vector a (S n)

This says that an element cons a vector of any size results in a vector that is guaranteed to be non-empty. This means that you could safely write a function to retrieve the head of a list by restricting the type to lists that are guaranteed to be non-empty.

    head : Vector a (S n) -> a

Something like the following pseudo-code in a REPL(I don't actually know a thing about Idris):

    let nums : Vector Int n = []
    head nums

...would fail to compile, since the second type param to nums is simply `n` rather than `(S n)`, as required by our `head` function. All of the things you would expect from Haskell like the power of ADTs and pattern-matching apply here, so you get even more compile time type-soundness.

[chriswarbo]

> For instance, the Vector type in Idris has two type parameters (not sure that's the correct term to use in this case): the first is the type of the element contained by the vector, and the second is the length of the vector.

In case anyone's wondering, only the first of these (the element type) is a type parameter, since it has a constant value in all sub-expressions (ie. the cons cells all contain elements of the same type).

The second is a 'type index', which is a more general term (type parameters are a special case of type indices), since its value changes in the sub-expressions (the cons cells have different lengths).

The difference is that we don't need to pattern-match parameters on every recursive call, since they're guaranteed to be constant (although we can if we like).

I didn't know this until I asked http://cs.stackexchange.com/questions/20100/what-are-the-dif...

[rybosome]

Makes sense; thanks for the clarification!

[JadeNB]

Without really addressing your question, notice that the power of dependently typed languages is not in the intelligence of the compiler, but in the expressivity of the type system. That is, the question becomes not "can the compiler catch this error on its own?", but rather "can the compiler verify my proof that I have not made this error?" A language with a very powerful type system can still have a very dumb compiler (although it will generate extremely slow code).

EDIT: It occurs to me that this is well summarised by the apparently facetious remark "Ask not what your compiler can do for you; ask what you can do for your compiler."

[RogerL]

In Ada you have subtype, so you would write

subtype my_type is Integer range 0..10; my_type x = 9; my_type y = 10; my_type a = x + y;

So, obviously there is enough information to deduce at compile time that the sum operation yields an incorrect value. In practice, as many of the replies point out, you can determine no such thing (my_type x = user_input()).

In that case Ada will throw a runtime exception. All this checking is expensive, so it ends up being much like C/C++, where you have debug and release builds, where the release builds do not do the checking.

[quandrum]

Yes

  int x (>= 0, <=10)
  x = parseInt(getKeyboardInput)

Dependent Type systems don't have to know what is possible keyboard input. They have to know what type the getKeyboardType function returns (and the parseInt), and if it's possible for that type to be out of the range of your constraint.

If that's so, it throws an error. At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.

[jarrett]

> if it's possible for that type to be out of the range of your constraint....If that's so, it throws an error.

If I'm understanding you correctly, that would seem to take a lot of the power out of dependent type systems. Almost all values will eventually depend on input from the outside world, so it seems you'd rarely have a chance to use your dependent type system.

Haskell (which doesn't have dependent types baked in) has a good approach to possibly-invalid data via the Maybe type. E.g. Maybe Int means "either an integer, or nothing." So it forces you to explicitly handle the possible error cases.[1]

To spell it out in Haskell terms: In the example of getting an integer from the keyboard, x is a Maybe Int. If the input is invalid, the value is set to Nothing, which is a unique constant. If it's valid, the value is of type Just Int.

> At that point you simply have to compose your types and functions so they match the constraint, and you know you are safe.

But how do you get from untrusted, potentially invalid data into the world of trusted, guaranteed-valid data? How do you bridge the gap? I was suggesting some combination of an applyConstraint function and a Maybe type to achieve that. Are there other ways?

[1] Actually, it will let you bypass the usual compile-time protections with the fromJust function. But if you want compile-time safety, either refrain from using fromJust, or use it only where you're absolutely sure the value won't be Nothing.

[Kutta]

> But how do you get from untrusted, potentially invalid data into the world of trusted, guaranteed-valid data?

The main point is that you can write provably correct validation functions. Then your program can branch on the result of that function, and in the "success" branch you can process data further, as usual, assuming (justifiably) the validity of the data. It doesn't make any difference whether some particular piece of data was validated runtime or compile time, so far as the validation does what you want it to do and the types reflect the result in sufficient detail. Verified programming is mostly not about trying to check everything compile time, but rather checking that when our program eventually runs, it does the right thing. Take the following pseudo-Idris-Agda function:

    boundsCheck : Nat -> (bound : Nat) -> Maybe (n : Nat ** n < bound)
    boundsCheck n b with n <? b 
        | yes proof    = Just (n , proof)
        | no  disproof = Nothing

This either returns the input natural number (if the input is within bounds) along with a proof of being in bound, or returns failure. The type of the function makes it impossible to write a function body such that the returned number is not within the supplied bounds. Any subsequent code in the program may work with the output of this function and be utterly sure that the "n" in "Just (n, p)" observes the bound, and the may also safely omit any further checks for the same bound or greater bounds. Or here's a standard Idris function:

    filter : (a -> Bool) -> Vect n a -> (n : Nat ** Vect n a)
    filter p [] = (_ ** [])
    filter p (x :: xs) with (filter p xs)
        | (_ ** xs') = if p x then (_ ** x :: xs') else (_ ** xs')

This is a plain old filter, except that it works on a length-indexed list type "Vect". We have no idea (compile time) how long the resulting filtered Vect will be. So we return a dependent pair containing some Nat and a Vect such that its length is equal to that Nat.

You might think that this is rather boring, since we could have used a list type not indexed by its length, and then just computed the length whenever we needed it runtime. Except there is a big difference. It is impossible to return a value of type

    (n : Nat ** Vect n a)

from any function, such that in the value the Nat index does not equal the length of the vector! You could slap together a plain list and a Nat in a tuple, and then say: "This a list coupled with its length. Let's try to preserve this invariant by writing code carefully". You could also trying hiding the possibly unsafe internals behind some OOP class firewall, but even that doesn't protect you from writing the internals incorrectly. Dependent types can protect you even then; they only fail to prevent you from writing the wrong types in the first place.

[pseudonom-]

As a sort of side note, why is it

    filter p (x :: xs) with (filter p xs)
        | (_ ** xs') = if p x then (_ ** x :: xs') else (_ ** xs')

rather than

    filter p (x :: xs) = if p x then (_ ** x :: snd (filter p xs)) else (_ ** snd (filter p xs))

?

[Dewie]

I think a better example is the partial functions in Haskell like head or tail. They throw an exception on empty lists. You could make it return maybe [a] or a default value, but a common usage of head might be where you know yourself that the list is non-empty. Like:

head . sort . f

where f is a function that you know returns a non-empty list, perhaps because that's just the way it operates or because you checked it further up. You know that head won't crash since any reasonable implementation of sort returns a list which is just as long as the one that was given to it. Similarly:

tail . sort . f

won't crash. Moreover, the list will still be sorted, since you just removed the head of the list.

This is all known to you, but you can't necessarily easily show it to the compiler.

I don't know the motivation for wanting to know the input before it is given. Putting it in a Maybe is the only sensible option. Some things are just not known/unknowable before running a program. You wouldn't even need to run the program if you could prove absolutely anything about the properties of a program.

Will the user input bleed through to all corners of the program? Well, why would it? You could have a sanitizing loop that refuses to pass "wrong" data to the pure (and dependently typed!) parts of the program, just looping over and over until the correct input is given.

[dllthomas]

"You wouldn't even need to run the program if you could prove absolutely anything about the properties of a program."

That's not really true.

[arh68]

> Can a dependent type system catch all type errors at compile time?

I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

> because the value of getKeyboardInput could be anything

That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration:

    x = (parseInt(getKey) :: Int(>=0, <=10))

Then you type-annotate everything you can, marking every non-annotated expression as wild:

    w = ... :: Int(>=0, <=10)
    x = ... :: Int(>=0, <=2)
    z :: Int(>=0, <=20)
    y = w * x                 -- :: Wild
    z = y                     -- compiler should Scream!

Asking the compiler to infer arbitrary type declarations seems hard. I think y probably shouldn't be inferred as :: Int(0<=..<=20) unless there is a rule somewhere that Int(a<=..<=b) * Int(c<=..<=d) = .. :: Int(f<=..<=g).

The work still needs to be done (no magic bullet here), but we should be able to use the computer to generate well-defined type combinations.

[leoc]

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

IIRC dependently-typed languages dodge this bullet by not being completely Turing-complete (as 'twere).

[chriswarbo]

Not quite. Many dependently-typed languages aren't Turing-complete, but that's no how they 'dodge this bullet'.

Think about the following Java code:

    public int getMyInt() {
      return getSomeOtherInt();
    }

How hard does Java have to work to figure out whether getMyInt is well-typed? Does it have to solve the halting problem? No. It just checks the information that you have given it. If you wrote that getSomeOtherInt has return type "int" then getMyInt will type-check. If you gave it some other type, it won't type-check. If you didn't give it a type, it will complain about a syntax error. At no point will Java try to write your program for you (which would hit against the halting problem). The same is true in dependently-typed languages, except the types happen to be much stronger. You still have to write them down, write down values of those types, write conversion functions when you need to combine different types, etc.

Incidentally, if a language is Turing-complete, it actually becomes really easy to get a program to type-check; we just write infinite loops everywhere, which leads to logical fallacies ;) That's why many dependently-typed languages aren't Turing-complete (although many are; eg. those which distinguish compile-time terms from run-time terms, like ATS).

[Ralith]

You can compromise on turing-completeness, too. Idris, for example, lets the programmer decide whether a given definition should be required to provably terminate or not.

[ufo]

The real way dependently typed languages dodge the undecidability problem is taht they "give up" on some valid programs. The output of the typechecker is either "proved the program is correct", "proved the program is incorrect" or "incondusive". If the result is "inconclusive" then it means that the programmer needs to manually provide a proof of correctness.

[mnarayan01]

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

Guessing you're plenty clever...just didn't think about it enough :)

Simply transform a program into one which halts on a type error rather than whatever else it might be doing. Done.

[samatman]

Consider the case of a simple type system, where any statement in the language is of either type "true" or type "false"....

[jessaustin]

This proof is missing a few steps, at least if it's meant to convince slow thinkers like myself. b^)

[dllthomas]

"Can a dependent type system catch all type errors at compile time?"

Provably not, if you want a type checker guaranteed to finish.

[jarrett]

Could you give a brief overview of why? Does this come down to the halting problem?

[arjunnarayan]

Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.

[Kutta]

Note though that undecidability is not really an issue in practice. You can always just refuse to run any function compile time that has not yet passed termination check. In fact Idris does exactly this. This already puts Idris ahead of C++ in terms of compilation termination, and it's not even like people are frequently disgruntled about diverging C++ templates.

[dllthomas]

"You can always just refuse to run any function compile time that has not yet passed termination check."

I don't understand this sentence.

[Kutta]

Both Idris and Agda check whether functions provably terminate. Halting problem notwithstanding it is possible to have conservative checks that never return false positives, so that an OK from the checker implies termination, but a FAIL doesn't imply non-termination.

Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to occasionally run Idris functions (that's what makes it dependent). This is in fact the only source of potential non-termination in the checker. So, whenever Idris needs to run a function compile time, and it cannot prove termination via the checker, it just throws an error.

(Side note: it is never required to run a function in order to the typecheck the very same function. All major dependent type checkers has the property that they never have to run a function that is not already checked).

[solomatov]

>Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.

In dependently typed programming languages like agda and Idris typechecking is decidable. You are wrong here.

[arjunnarayan]

You're right. I was being handwavey, and I apologize for that.

Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.

There's a reason dependent types haven't caught on in industry, and even the "fancy" types that are cited by proponents as being used in practice (like ML's Hindley-Milner type system) are MUCH simpler than full blown dependent type systems. Because the burden is shifted to the programmer, and that makes it super unusable.

I'm not a dependent types hater. (I have dependent type friends :) ). But the best way to get a usable type system is to restrict it's expressivity to make automation easier, and the annotation burden much smaller. Sure, we're giving up something there. But it's better than having a system that can prove any theorem in the Calculus of Constructions, but used by about thirty people.

[solomatov]

>Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.

That's why we need gradual typing. Some critical parts should be written with full dependent types with termination checker, etc, but most of the code should be just type checked.

P.S. I have some dependent types experience, including applying Coq in commercial projects.

[dllthomas]

You're right with a strict reading. "In general, dependent types ..." should be a statement about all instances of "dependent types" or (weakening to one common English usage) a statement about typical instances of "dependent types". In neither case, are they undecidable.

A loose reading (probably overly loose, but possibly what was intended rather than what was expressed) would permit something closer to "Dependent types, in full generality, are undecidable to type check." which I believe to be the case, where actual implementations are more constrained (though decreasingly so!).

[nuncanada]

Yes, Depently Typed languages can. They are full blown theorem provers...

[JadeNB]

Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems.

(This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't need the full Gödelian power to observe that a priori theorems that must be verified at compile time can never account for data that are provided only after compilation.)

[sold]

When I write a program, I don't want it to be just correct (true); I want it to be _provably_ correct; I want to be able to be convinced that it is correct, at least in principle, given enough time and whole specification of the system. Programs which are correct, but not provably so, should not pass code review and might as well be lumped together with those which are wrong. It doesn't matter if you are using a full-blown theorem prover or thinking about the code in your head; Gödel's theorems are not really relevant to programming, even when the code uses deep mathematics.

I'm not sure I agree with "theorems that must be verified at compile time can never account for data that are provided only after compilation". At compile time, you prove the assertion "for every x, the program outputs correct answer for x". Now, you don't know that the user will enter say x=5 at runtime, but since you proved a theorem about _every_ x, this includes x=5. You cannot predict the future (the path that will be taken by the program), but once you prepare for all possible futures, you're safe.

[platz]

The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system.

I hear Idris is more reasonable in this regard and has better general purpose programming properties.

[solomatov]

>The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties.

You can say the same for any strongly typed language, but reality is it's the opposite. If your program has a good design, it's easy to refactor.

[platz]

source: http://www.johndcook.com/blog/2014/02/10/real-world-haskell/...

[jarrett]

> can never account for data that are provided only after compilation

It seems to me they could. Suppose my program depends on external input D. That input could be a file it loads, keyboard input, network input, or anything else. Could I declare that I expect D to have properties P? And then, could the language force me to implement a code path for cases where D does not satisfy P? An example of such a code path would be to print an error message and then terminate the program.

[JadeNB]

Yes, this is a good point. I hope that what I meant was reasonably clear, but a more precise would have been something like "cannot prove certain assertions about data that are provided only after compilation".

[solomatov]

>Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems.

They don't prove theorems. You do this by writing a program.

[JadeNB]

Sure, but, regardless of agency, human or automated, it is still not possible to prove all true theorems. (The human / automated distinction comes in more sharply in the halting problem, where any potential halting decider will choke on some program that proveably terminates.)

[Dewie]

I wonder; have mathematicians found something that they know with every fibre of their being is true, but that they can't prove? And do they then try to prove it in another formal system instead?

Or do these unprovable-but-true facts mostly elude them, since they are operating in a formal system that 'hides' them?

[lmkg]

There are a couple of statements that have been proven to be unprovable in the standard axiom set (ZF). The provability of the unprovability of unprovable statements is not guaranteed, but happens to be true for many of the more useful axioms.

The most common is the Axiom of Choice, which if true is incredibly convenient. For example, the Axiom of Choice implies that all Vector Spaces have a basis, which makes linear algebra tractable. Mathematicians generally accept it as true because it's useful and intuitively true, but it does have some consequences that are intuitively false, like the Banach-Tarski paradox. We even have a saying: "The Axiom of Choice is obviously true, the Well-Ordering Principle is obviously false, and Zorn's Lemma no one even knows." The implicit punchline being, these three things are logically equivalent because each implies the other.

Other axioms that are independent of ZF include the Continuum Hypothesis and the Axiom of Foundation. The Continuum Hypothesis says that there is no type of infinity that is larger than the cardinality of the Rationals and also smaller than the cardinality of the Reals. It doesn't make a damn lick of sense for such a type of infinity to exist, but it's not technically possible to disprove it. The Axiom of Foundation, in very simple terms, disallows objects like "the set that contains itself." Such sets are not constructable in ZF, and are logically impossible, but they are not technically disallowed.

Using "stronger" axiom sets to investigate the properties and consequences of these unprovable statements is common. Additionally, many automated theorem-provers include several of the more convenient axioms that aren't included in "regular" mathematics.

More reading: http://en.wikipedia.org/wiki/List_of_statements_undecidable_...

(Note: ZFC is ZF plus the Axiom of Choice; Choice is so damn convenient that the mathematics establishment usually accepts it by default, although proving that you don't need Choice to prove something is often seen as a worthwhile accomplishment.)

[cpa]

Mathematicians say that formula F is true in system S iff one can find a proof of F in the context S. So truthness is always considered with respect to some system. Thus, there are no formula which is "true" but that one can't prove, by definition. (That's the kind of smartassery mathematicians like.)

But the Godel's incompleteness theorem states that for all system that includes (Peano's) arithmetic, one can find a formula in this system that has cannot be proved and whose contrary cannot be proved either. And to answer your question, Godel's proof explicitly shows such a formula.

[JadeNB]

Words in mathematics mean what they are defined to mean, so there's no point arguing about the correctness of definitions. Yours is essentially the constructivist perspective on truth; but it is not the only one. It will declare that certain statements are neither true nor false, which some find distasteful.

A more model-theoretic approach says that a formula is true in a theory (not a system, although the word choice doesn't matter) if it is true in all models of that theory—a statement that can (in principle) be concretely verified simply by testing in each such model. Then it may (and will) be true that a statement is true in "all possible worlds", but that there is no way of proving it from the rules that constrain 'possibility'.

[randyrand]

| int x (>= 0, <=10) | x = parseInt(getKeyboardInput)

Will be a compile time error because getKeyBoard input returns integers that are between 0-256(?) not 0-10 like 'x' wants.

[jarrett]

Exactly. That's why I proposed a Haskell-ish Maybe construct to represent the uncertainty of the input's validity. The code snippet:

  int x (>= 0, <=10) | x = parseInt(getKeyboardInput)

...was meant as an example of what won't work.