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