3 ms·

Anyone know how runtime IO errors would be handle with dependent types? You can't prove that an outside source is going to return what you expect. Would you j

• freyrs3 12y ago
  You can however obligate that the function that invokes the outside IO be required to return valid input as a constraint in the type-system. So you wouldn't be able to compose an unrestricted ``readLine`` function with a function that couldn't handle the invalid input. It's shifting the checks to ensure that the invalid program is completely inexpressible by construction instead of ensuring runtime safety like a Maybe would.
• skybrian 12y ago
  We do something sorta like this in GWT by having a SafeHtml type to represent trusted HTML. To take untrusted HTML and convert it to SafeHtml, you have to sanitize it. In Java, we have a few trusted methods to do this and don't actually prove it, except informally in code review. In the old days, Perl had a "taint" mode that did similar things. I imagine that in a dependently typed language, you'd have a lot of input validators that return either a proof of validation or an error to report back to the user. It clarifies which parts of the program assume "safe" input and what that means, allowing you to restructure your program. But it doesn't get rid of input validation, just moves it around.
• chriswarbo 12y ago
  It helps to remember that we don't gain any expressiveness from a type system, only safety[1]. Type systems can only restrict which programs we're allowed to write[1], compared to un(i)typed programs. After our programs have passed the type-checker, their types can be erased to leave behind a raw un(i)typed program. In the case of functional programming, we can imagine it compiling down to something like Scheme. The point is that we can handle error conditions just like we do in any other language: if we're compiling to something which looks like Scheme, we can handle errors in the same way: have everything return a sum allowing errors (ie. a Maybe). Even things which don't produce errors can be lifted to this type automatically and chained together using a monad. That's basically what Haskell does. Of course, lifting simple functions to return Maybes isn't very nice, since we're purposefully throwing away information; ie. we're causing our consumers to ask "did this return a value or not?" when we already know that it always will. The problem is that with composing Maybe functions with simple functions. There's no way around this in Haskell, we need to lift the simple functions; after all, that's the point of a monad: we can return a wrapped value and we can join a wrapped-wrapped value into a wrapped value but there's no way to unwrap a value (otherwise we may have a comonad instead!). Dependent types give us more flexibility than Haskell though: if our output value depends on the input, we can also make our output type depend on the input. For example (where "A", "B" and "C" are some concrete types, for simplicity): -- Simple function myFunc1 : A -> B myFunc1 = ... -- Maybe function (ie. might error) myFunc2 : C -> Maybe A myFunc2 = ... -- Maybe monad. Works, but loses some type info liftedChain : C -> Maybe B liftedChain x = case myFunc2 x of Nothing -> Nothing Just y -> Just (myFunc1 y) -- Exactly the same algorithm, but without losing type info myType : Maybe A -> Type myType Nothing = () -- Unit type, equivalent to Nothing myType (Just _) = B -- Result type, equivalent to Just unliftedChain : (c : C) -> myType (myFunc2 c) unliftedChain x = case myFunc2 x of Nothing -> () -- Unit value; matches myType Nothing as required Just y -> myFunc1 y -- Value of type B; matches myType (Just y) as required This makes it easy to handle runtime errors, without having to pretend that everything else might blow up. Typically, we write most of our code in an ideal world assuming all of our requirements are met, then we write simple "driver" functions which justify those assumptions, returning errors otherwise. Exactly like in Haskell, where we write pure functions for manipulating plain values like strings, then write simple "driver" functions to pull those strings out of files, databases, sockets, etc. using IO. [1] Strongly typed languages can be more or less expressive than each other due to their type systems (eg. dependent types make it easy to express homogeneous lists, which can't be done (AFAIK) in System F), but all are less expressive than un(i)typed languages.
  • seanmcdirmid 12y ago
    > It helps to remember that we don't gain any expressiveness from a type system, only safety[1]. That is controversial, especially when you are considering non-safety oriented tools like code completion systems or program inference engines. Languages with reified types may also make decisions at run-time based on the actual type of a value (e.g. virtual method dispatch).
    • chriswarbo 12y ago
      I meant "expressiveness" purely in the sense that "we can write more programs 'without' types than with them" (of course, the types are 'still in there somewhere'; we're just ignoring them). I wasn't referring to external tooling, which I agree gains a lot from strong types (specifically because a load of programs have been forbidden, which makes their job tractable). When dependent types and proving correctness are mentioned, there is often an assumption that some magical ability is gained. For example, all the questions here about error handling. Dependent types don't handle errors, they're just types; but what they can do is forbid code which doesn't handle errors. As for "reified types" affecting run-time behaviour, I would call those tags rather than types. For example, the class of an object is a tag, not a type.
      • seanmcdirmid 12y ago
        > I wasn't referring to external tooling, which I agree gains a lot from strong types (specifically because a load of programs have been forbidden, which makes their job tractable). Careful. You also want to allow unsound choices in completion options, since the programmer could have made a mistake or is unaware of the more specific type needed to support some operation (especially if they are using code completion for discovery purposes). Sometimes the path between valid program A and valid program C is an invalid program B (think about editing code without the ability to create transient syntax errors...how horrible would that be!). Type theorists often get this wrong, because they are so focused on correctness :) > When dependent types and proving correctness are mentioned, there is often an assumption that some magical ability is gained. I thought magic was needed just to do the type checking. I don't think anyone who has gone through the program proving process would think it was easier (e.g. via F*), a lot of sweat is required to get those rock solid absolute guarantees. > As for "reified types" affecting run-time behaviour, I would call those tags rather than types. For example, the class of an object is a tag, not a type. This is only the overly narrow type theorist's definition of type. The class of an object is obviously a type/kind/classifier via the informal definition of type. In a statically typed language, it also happens to correspond 1-1 with the static type of the object as created, which is incredibly useful from a usability standpoint. Erasure likewise is pretty bad, and languages that don't erase (C# vs. Java) are much more usable.