8 ms·

Dependently Typed Programming

70 points by waffle_ss 12y ago

coolsunglasses 12y 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-Sendai 12y 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 12y ago
  "and to terminate" That must be a neat trick - or you've constructed a non-Turing -complete language...
  - skew 12y 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.
    - tel 12y ago
      It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.
      - Ono-Sendai 12y ago
        Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..
    - dllthomas 12y ago
      "(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)" Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".
  - eru 12y ago
    Finding non-Turing complete, but still interesting languages, is a noble pursuit.
    - tel 12y ago
      Why? PFPL has like 10 chapters on them. It's never really been stated why Completeness is a good thing.
      - eru 12y ago
        Yes. It's a useful endeavour. Things like Datalog, regular expressions or applicative parser combinators come out of it.
  - qu4z-2 12y ago
    Or it just refuses to compile/execute something it can't prove terminates.
    - TheCoelacanth 12y ago
      That would make it non-Turing complete. Of course there probably aren't many interesting programs that are ruled out by that restriction.
      - marcosdumay 12y ago
        There are many interesting programs that don't ave any guarantee that they terminate. A a few that don't really terminate, ever. In fact, if you click on the launcher menu on your computer, I'll bet most programs there just keep going, until some random event (AKA clicking on an "x") throws them out of the loop.
        TheCoelacanth 12y ago
        It wouldn't require that all programs terminate, just that all functions terminate.
        marcosdumay 12y ago
        Your programs aren't composed of one top-level function?
        TheCoelacanth 12y ago
        More likely they would be composed on one top-level IO value, like in Haskell, or something similar.
        eru 12y ago
        That's why you'd ask your programs to be `productive'. Also look up co-recursion and co-data, if you want to find out more about this. (It's basically the logical way to extend `termination' from batch programs to things like continuously running programs like operating systems.)
  - Ono-Sendai 12y ago
    Yeah, it's non turing-complete.
mamcx 12y 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?
- chriswarbo 12y 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-blindness/ http://existentialtype.wordpress.com/2011/03/15/boolean-blin...
- jonsterling 12y 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"
peaton 12y 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?)
- munro 12y 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.
  - peaton 12y ago
    That's a little vague, I think. Pure functional programming has no side effects. Isn't that as succinct & thorough as it gets?
    - dllthomas 12y ago
      "Pure functional programming has no side effects." Well... every program has side effects when you run it - I don't yet know a language with a type system that reifies CPU temperature. I think it might be correct to say that idealized pure functional programming doesn't rely on side effects for correctness?
      - munro 12y ago
        It makes more sense if you think of your program as schematics for building a machine. Following that metaphor, the type system can help you find flaws in your design. When you build your schematics, you're still constrained by the real world, unfortunately. CPU temperature would just be an IO request, which leaves your program, the runtime collects the information, then feeds it back into your program. I personally like to think of my machine running in a lab, with IO being scientists running around taking data out, doing work, then feeding it back into the machine. :D
        dllthomas 12y ago
munro 12y 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 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.
peaton 12y 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.pdf http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper... [2] http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf
- gtani 12y ago
  this idris paper, maybe, or how is security guaranteed? http://www.simonjf.com/writing/bsc-dissertation.pdf http://www.simonjf.com/writing/bsc-dissertation.pdf quote: enforce resource usage protocols inherent in C socket programming, providing safety guarantees,
  - peaton 12y 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 12y 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 12y 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 12y ago
    > What "dependable imperative languages" do you use in practice that offer better maintainability than Haskell? Scala
  - felixgallo 12y ago
    Erlang
- tel 12y 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 12y 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.
- seanmcdirmid 12y 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).
  - chriswarbo 12y 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).
peterashford 12y 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?
- dllthomas 12y 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.
- tel 12y 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.

70 points by waffle_ss 12y 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-Sendai 12y 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 12y ago
"and to terminate" That must be a neat trick - or you've constructed a non-Turing -complete language...
- skew 12y 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.
  - tel 12y ago
    It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.
    - Ono-Sendai 12y ago
      Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..
  - dllthomas 12y ago
    "(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)" Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".
- eru 12y ago
  Finding non-Turing complete, but still interesting languages, is a noble pursuit.
  - tel 12y ago
    Why? PFPL has like 10 chapters on them. It's never really been stated why Completeness is a good thing.
    - eru 12y ago
      Yes. It's a useful endeavour. Things like Datalog, regular expressions or applicative parser combinators come out of it.
- qu4z-2 12y ago
  Or it just refuses to compile/execute something it can't prove terminates.
  - TheCoelacanth 12y ago
    That would make it non-Turing complete. Of course there probably aren't many interesting programs that are ruled out by that restriction.
    - marcosdumay 12y ago
      There are many interesting programs that don't ave any guarantee that they terminate. A a few that don't really terminate, ever. In fact, if you click on the launcher menu on your computer, I'll bet most programs there just keep going, until some random event (AKA clicking on an "x") throws them out of the loop.
      - TheCoelacanth 12y ago
        It wouldn't require that all programs terminate, just that all functions terminate.
        marcosdumay 12y ago
        Your programs aren't composed of one top-level function?
        TheCoelacanth 12y ago
        More likely they would be composed on one top-level IO value, like in Haskell, or something similar.
      - eru 12y ago
        That's why you'd ask your programs to be `productive'. Also look up co-recursion and co-data, if you want to find out more about this. (It's basically the logical way to extend `termination' from batch programs to things like continuously running programs like operating systems.)
- Ono-Sendai 12y ago
  Yeah, it's non turing-complete.

mamcx 12y 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?

chriswarbo 12y 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-blindness/ http://existentialtype.wordpress.com/2011/03/15/boolean-blin...
jonsterling 12y 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"

peaton 12y 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?)

munro 12y 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.
- peaton 12y ago
  That's a little vague, I think. Pure functional programming has no side effects. Isn't that as succinct & thorough as it gets?
  - dllthomas 12y ago
    "Pure functional programming has no side effects." Well... every program has side effects when you run it - I don't yet know a language with a type system that reifies CPU temperature. I think it might be correct to say that idealized pure functional programming doesn't rely on side effects for correctness?
    - munro 12y ago
      It makes more sense if you think of your program as schematics for building a machine. Following that metaphor, the type system can help you find flaws in your design. When you build your schematics, you're still constrained by the real world, unfortunately. CPU temperature would just be an IO request, which leaves your program, the runtime collects the information, then feeds it back into your program. I personally like to think of my machine running in a lab, with IO being scientists running around taking data out, doing work, then feeding it back into the machine. :D
      - dllthomas 12y ago

munro 12y 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 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.

peaton 12y 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.pdf http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper... [2] http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf

gtani 12y ago
this idris paper, maybe, or how is security guaranteed? http://www.simonjf.com/writing/bsc-dissertation.pdf http://www.simonjf.com/writing/bsc-dissertation.pdf quote: enforce resource usage protocols inherent in C socket programming, providing safety guarantees,
- peaton 12y 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 12y 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 12y 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 12y ago
  > What "dependable imperative languages" do you use in practice that offer better maintainability than Haskell? Scala
- felixgallo 12y ago
  Erlang
tel 12y 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 12y 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.

seanmcdirmid 12y 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).
- chriswarbo 12y 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).

peterashford 12y 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?

dllthomas 12y 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.
tel 12y 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.