Dependently Typed Programming

http://ejenk.com/blog/why-dependently-typed-programming-will-one-day-rock-your-world.html

by waffle_ss • 12 years ago

70 75 12 years ago

proof that your program will terminate

Or that a coprogram will be productive (services/servers/streaming fall under this).

Most programs these days operate on codata, so termination on a per-destructed-codata-component basis is productivity if I understand correctly.

(ejenk touches on this in the comments as well, but I wanted to add this point)

Ono-Sendai3• 12 years ago

My language works a little like this. All programs are verified to be safe (not crash, read out of bounds, etc), and to terminate.

al2o3cr• 12 years ago

"and to terminate"

That must be a neat trick - or you've constructed a non-Turing -complete language...

skew• 12 years ago

Non-Turing-complete is not a bad way to go. You pretty much have to already be a researcher in dependent type systems (or maybe set theory) to invent functions that always terminate but can't be written in non-Turing-complete languages like Coq (an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of). Also, writing a program that proves some programs terminate is way easier than proving a program that correctly proves any terminating program terminates, if you are confusing the two. If it's not too common, "I didn't manage to prove this terminates" sounds like a reasonable compiler error.

eru3• 12 years ago

Finding non-Turing complete, but still interesting languages, is a noble pursuit.

qu4z-22• 12 years ago

Or it just refuses to compile/execute something it can't prove terminates.

Ono-Sendai3• 12 years ago

Yeah, it's non turing-complete.

mamcx3• 12 years ago

I have think in something like this, but far simpler: Why the (avg) languages can't define types like in a database language? (ej: Age:Int, Check: x > 0 & x < 200).

However, with this: I get how can be usefull for data directly in the code, but how this work with data that come from somwhere? If i feed a CSV with numbers, what happend when some is 0?

chriswarbo6• 12 years ago

However, with this: I get how can be usefull for data directly in the code, but how this work with data that come from somwhere? If i feed a CSV with numbers, what happend when some is 0?

The same thing that happens in any language; have a validation layer which checks whether the incoming data is zero or not. If it is, then do something appropriate (eg. print an error and halt), if not then you can safely pass if to your non-zero function.

See http://existentialtype.wordpress.com/2011/03/15/boolean-blin...

jonsterling• 12 years ago

So the way it works when your data comes from somewhere and you don't know if it is "clean" is that you write a decision procedure to "find out".

So the simplest use case is you've got a type like `{x : String | x.length < 10}`: that is, the type of strings which have length less than ten. A value of that type is going to be a pair `<str, proof>` where `proof` is an object which witnesses the fact that `str` has a length less than ten.

Now, it is a decidable property whether or not a string is shorter than 10 chars long. You can easily construct a function with the following type:

    decideValidity : (str : string) -> Either (str.length < 10) (Not (str.length < 10))

This function is defined by induction on the string.

Now you want to receive such a string from user input. Crucially, the logic of your program is going to operate on data that's already been validated: so your program will only deal with `{x:String | x.length < 10}`; we just need to shore up the boundaries between your program and user input.

    yourComputation :: {x:String | x.length < 10} -> Something

    main : IO ()
    main = do
      userInput <- getLine
      case (decideValidity userInput) of
        Left prf -> do
          print (yourComputation <userInput, prf>)
        Right nope -> 
          print "The input was invalid"

munro6• 12 years ago

Is it possible with Idris to programmatically create the `decideValidity` function? Conceptually it seems trivial to do, I could imagine building it with meta programming. My crazy pseudo code-- :D

    decideValidity : (p : Proof) -> a -> Either (p a) (Not (p a))

mamcx3• 12 years ago

But then, I don't see what I gain with this. Is like have Eiffel contracts.

lobster_johnson2• 12 years ago

Pascal, and Pascal-derived languages such as Modula and Turbo Pascal, have this:

    type Age = 1..199;

A value of type Age can only have the values 1 <= x <= 199, and can't be assigned to non-Age variables. Enums belong to this category of ordinal types.

In Ada:

    type Age is Range 1 .. 199;
    type Temperature is new Integer Range 32 .. 212;

    a: Age; t: Temperature
    a := t  -- this fails at compile time

Ada 2012 adds the support for specifying Eiffel-style contracts, but on types:

    subtype Even is Integer
      with Dynamic_Predicate => Even mod 2 = 0;

You can't assign an odd number to a variable of type Even.

mamcx3• 12 years ago

Yep, I know about pascal (my 2d language after foxpro) but not the ADA 2012.

The Dynamic_Predicate is on runtime or compile time? If assign a:Int = Even, I need to be explicit and do a convert (I imagine is yes, that is the pascal style but not have experience with ADA)

peaton5• 12 years ago

In a functional language, you describe the problem to the computer, and it solves it for you.

Isn't this the definition of a declarative programming paradigm? (I.e. SQL?)

munro6• 12 years ago

I had the same thought, seemed off. What I think of "functional programming", and how it seems to be used, is that a function has to be pure.

peaton5• 12 years ago

That's a little vague, I think. Pure functional programming has no side effects. Isn't that as succinct & thorough as it gets?

UberMouse• 12 years ago

According to Wikipedia Functional Programming fits under the Declarative Programming paradigm. I'm not sure how accurate that is, but it seems to hold some truth.

"Functional programming, and in particular purely functional programming, attempts to minimize or eliminate side effects, and is therefore considered declarative."

"While functional languages typically do appear to specify "how", a compiler for a purely functional programming language is free to extensively rewrite the operational behavior of a function, so long as the same result is returned for the same inputs."

peaton5• 12 years ago

Ah, I see. That last bit is especially interesting.

I would argue that there are many languages (and no reason they couldn't) act otherwise with regard to that second quote. However, the line between pure functional and not starts to become fuzzy as well.

tel11• 12 years ago

Meh. "Declarative" and "functional" are such weak technical terms that it's tough to say whether or not that's true. Or whether or not seeking the truth of such a statement is itself even meaningful.

munro6• 12 years ago

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 just prove that it essentially returns a "Maybe" ?

Haskell exceptions have always weirded me out, I've poked at Idris, but plan to write a side project in it soon!

freyrs3• 12 years 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• 12 years 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.

chriswarbo6• 12 years 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.

seanmcdirmid4• 12 years 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).

peaton5• 12 years ago

UPenn has a ton of really interesting work on extending the Haskell type system to support dependent typing. Some of the coolest pieces I've heard about had to do with guaranteeing the security of a server application through dependent typing.

I never found out what the actual paper or project was that accomplished this. But these two papers[1][2] seems pretty interesting - having to do with guaranteeing safety of database access.

[1] http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper...

[2] http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf

gtani• 12 years ago

this idris paper, maybe, or how is security guaranteed?

http://www.simonjf.com/writing/bsc-dissertation.pdf

quote:

    enforce resource usage protocols inherent in 
    C socket programming, providing safety guarantees,

peaton5• 12 years ago

Hmm, I don't believe so. My prof went on about a group at Penn using dependent types to prove the security of server applications. But that is definitely an interesting paper too. Thanks for sharing!

MetaCosm• 12 years ago

Dependently typed programming already rocks my world -- but not my job.

I enjoy Haskell.... as a hobby. Whenever I am playing with it -- I distinctly understand that "it" is the point. The focus is squarely on the language and the programmers. I absolutely think this has a place, and I am delighted it exists. I remember the ... purity of my first little chess engine I wrote in it -- how it itched the OCD spot in my brain so perfectly, it made me exceptionally happy.

That said, when I am programming "in the wild"... the language is almost never the point. The application is the point, the library is the point, the problem domain is the point, the user is the point. Cleverness matters little, often what needs to be done is obvious and tedious. The biggest problems tend to be maintenance in every sense of the word... how to you maintain this if you are successful (multiple data centers, dozens of employees). How do you avoid rewriting everything at each major growth spike.

This means I use boring dependable imperative languages for what I bet my business (start-up) and future on -- and I spend my hobby time using far sexy functional languages... but I don't confuse my love for them with thinking they are a good fit for my business.

squidsoup• 12 years ago

Presumably one of the advantages of choosing a language with a strong type system like Haskell is that it would allow for better maintenance and refactoring. What "dependable imperative languages" do you use in practice that offer better maintainability than Haskell?

virtualwhys• 12 years ago

What "dependable imperative languages" do you use in practice that offer better maintainability than Haskell?

Scala

felixgallo• 12 years ago

Erlang

tel11• 12 years ago

Haskell is not really dependently typed. You can mimic it a bit, but you owe it to yourself to try reading through something in Coq or Agda (and maybe eventually Idris).

TacticalCoder• 12 years ago

Interesting article. Note that the article describes the maybe monad as used in Haskell and explains what it solves and then comes with this criticism:

"...we still need to run the program to observe that the computation fails somewhere and then figure out what happened"

As if figuring out where a problem happened was an issue in Haskell (or, really, in any language supporting something like the maybe monad).

If figuring out what happened when something failed is complicated because there were several maybe monads and in the end you got nothing, then Haskell solves this very nicely if I'm not mistaken: there's "Either", which can carry an error message along with the fact that there's no result.

Now I'm not disputing that a proof that something cannot happen would be great (and hence in this case not requiring Maybe / Either): all I'm saying is that people shouldn't misread that thinking that Haskell has no clean way of reporting why nothing got returned.

seanmcdirmid4• 12 years ago

If figuring out what happened when something failed is complicated because there were several maybe monads and in the end you got nothing, then Haskell solves this very nicely if I'm not mistaken: there's "Either", which can carry an error message along with the fact that there's no result.

Does that really work? Say you have an error in a long pipeline, wouldn't "Either" cause processing down the line to treat the error as valid data (the error wouldn't be None)?

What you really want is a maybe monad where you can propagate wither a Valid answer or an Error condition, where operations on the value merely propagate the error condition. Also, it would be nice if the monad was integrated into a debugger so the error condition could carry along enough context to allow the user to jump to execution context where the error occurred during debugging (if we are talking about programmatic errors, a distinction must be made between errors of programming vs. exceptions from the environment that can/should be handled).

chriswarbo6• 12 years ago

If the pipeline is constructed with fmap, <*> or >>= then the pipeline's constituents will only be applied to Right values. An error (a Left value) will short-circuit the pipeline and be returned as-is.

Alternatively, we could be more fancy and branch such that errors received their own, separate, processing (eg. logging).

tel11• 12 years ago

Either tends to be used for error conditions that arise from the outside—after all, you are (a) explicitly denoting them and (b) presumably handling them. Programmer errors tend to arise in invariant violations. Sometimes these are marked with `error "cannot occur"` or silly things like that. Dropping into a debugger here would be tremendous.

chriswarbo6• 12 years ago

The point is that in Haskell, once you start chaining Maybes together you are forced to deal with the Nothings, even if they won't actually arise.

For example:

    :t Data.Map.lookup 123 (singleton 123 "hello")
    Data.Map.lookup 123 (singleton 123 "hello") :: Maybe [Char]

Even though this lookup will clearly succeed, I am forced to handle the Nothing case. Dependent types let me encode more information about the value in my types, providing evidence that it will always be a Just, which I can use at compile time to convince the type checker that the Nothing case is unreachable.

As soon as the Nothing case is unreachable, I can easily unwrap the Maybe, since my only remaining branch is a "Just x", so I can simply return "x".

codygman• 12 years ago

fmap is very useful for dealing with Maybes also:

  Prelude M> import qualified Data.Map as M
  Prelude M> let val = M.lookup 123 (M.singleton 123 "hello")
  Prelude M> fmap reverse val
  Just "olleh"

So this means that you only deal with the chained maybes at the top level or in a call-site that needs to know a Nothing existed as the Nothings are propagated.

andrewflnr• 12 years ago

I don't think that's what the author meant in that passage. They're not bemoaning error reporting, they're complaining about the fact that you have to run the code to find out if there was a problem, rather than finding out at compile time. Having to track down the source of the runtime error is a minor injury in comparison.

peterashford• 12 years ago

Maybe I'm missing the point of Dependent Types and there's more to it than I understood from the article, but in the example given of a divide function that requires a proof of a non-zero denominator: isn't this already achieved by languages that employ design by contract, such as Eiffel?

dllthomas7• 12 years ago

My understanding of DbC in Eiffel is that checks are done at runtime, rather than having a proof at compile time that the behavior cannot occur.

tel11• 12 years ago

Eiffel can promise that it will halt at runtime if a contract is violated. DT languages can promise that no contracts could ever be violated by any possible runtime evaluation pathway.

The latter is much stronger, but weird sounding. What it typically means is that you are required to not cut corners. The type system will detect your failure to handle edge cases and refuse to compile until you either handle or explicitly ignore them.

Dependently Typed Programming

Related Stories