4 ms·

Certainly very sensible points. But I take some issue with the bits towards the end: > Fetishising Curry-Howard Hey, I happen to find Curry-Howard sexy, you h

Certainly very sensible points. But I take some issue with the bits towards the end: > Fetishising Curry-Howard Hey, I happen to find Curry-Howard sexy, you have no right to shame me! > To specify and check liveness or reachability, we need to represent programs as some kind of flow graph, where flows are very likely to span multiple functions and multiple modules. But no, this is exactly what basing systems on Curry-Howard (with terminating functions) buys you. If I give a HTTP response handler in Coq the type HttpRequest -> HttpResponse I know it is live, because the function is total. And similarly, dead code paths can be gotten rid of by eliminating a proof of False. So this lets you state liveness and unreachability. Of course, the proofs of those statements is very different from program-analysis-style systems. In a whole-program analysis, the analyser goes over the entire program, and at the end it says "well, I could not find anything calling this function, so I guess it's dead". In a Curry-Howard-style system, you need to look at the function and figure out when it should be called and what preconditions need to be true for it to work properly. But this is exactly why people like type systems, you can think about programs modularly rather than all at once.

skybrian 12y ago
I suppose, but outside certain mathematical systems that are designed that way, assuming that all functions are total is unrealistic. The languages we use every day are Turing-complete languages and infinite loops can happen.
- vilhelm_s 12y ago
  You don't have to assume everything is total, you just need to track in the type system which things are and which aren't. E.g. you could also give it the type HttpRequest -> IO HttpResponse where IO is some type allowing nontermination (e.g. defined coinductively along the lines of http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIntensiveMeeting.pdf http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIn...). Having a type for total functions gives you the option to state and prove totality properties, even if you maybe don't want to go through the effort of doing that for every function you write.
  - seanmcdirmid 12y ago
    Koka [1] does this; I find Daan's experiences in using it to build Madoko [2] to be very enlightening. Basically, I think he had to give up on total-ness more than he would have liked. [1] http://research.microsoft.com/en-us/projects/koka/ http://research.microsoft.com/en-us/projects/koka/ [2] http://madoko.codeplex.com/ http://madoko.codeplex.com/
  - chriswarbo 12y ago
    You don't need to go all the way to IO, you can make every function total using Partial: data Partial a = Now a | Later (Partial a) It's straightforward to do things in Partial, since it's a Functor, Applicative and Monad: instance Functor Partial where fmap f (Now x) = Now (f x) fmap f (Later x) = Later (fmap f x) instance Applicative Partial where pure x = Now x (Now f) <*> (Now x) = Now (f x) (Later f) <*> x = Later (f <*> x) f <*> (Later x) = Later (f <*> x) instance Monad Partial where return = pure f >>= (Now x) = f x f >>= (Later x) = Later (f x) Partial is so trivial that everything can be made co-recursive by wrapping all function bodies in "Later". All of the "Later" wrappers will get nested together by the Applicative/Monad; everything will "just work". The one missing piece is the following function, which isn't total: runPartial :: Partial a -> a runPartial (Now x) = x runPartial (Later x) = runPartial x We could name it `unsafeForcePartial` and treat it with care, like we currently do with `unsafePerformIO`.
    - throwaway283719 12y ago
      Can you explain how this makes every function total? For example, take the `head` function which is not total head :: [a] -> a head (x:xs) = x head [] = undefined How can you make this total using `Partial`? I can get as far as headTotal :: [a] -> Partial a headTotal (x:xs) = Now x headTotal [] = Later (...) but what goes in (...)?
      - pdpi 12y ago
        This is why it's always seemed to me that head ought to be typed as head :: [a] -> Maybe a

skybrian 12y ago

I suppose, but outside certain mathematical systems that are designed that way, assuming that all functions are total is unrealistic. The languages we use every day are Turing-complete languages and infinite loops can happen.

vilhelm_s 12y ago
You don't have to assume everything is total, you just need to track in the type system which things are and which aren't. E.g. you could also give it the type HttpRequest -> IO HttpResponse where IO is some type allowing nontermination (e.g. defined coinductively along the lines of http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIntensiveMeeting.pdf http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIn...). Having a type for total functions gives you the option to state and prove totality properties, even if you maybe don't want to go through the effort of doing that for every function you write.
- seanmcdirmid 12y ago
  Koka [1] does this; I find Daan's experiences in using it to build Madoko [2] to be very enlightening. Basically, I think he had to give up on total-ness more than he would have liked. [1] http://research.microsoft.com/en-us/projects/koka/ http://research.microsoft.com/en-us/projects/koka/ [2] http://madoko.codeplex.com/ http://madoko.codeplex.com/
- chriswarbo 12y ago
  You don't need to go all the way to IO, you can make every function total using Partial: data Partial a = Now a | Later (Partial a) It's straightforward to do things in Partial, since it's a Functor, Applicative and Monad: instance Functor Partial where fmap f (Now x) = Now (f x) fmap f (Later x) = Later (fmap f x) instance Applicative Partial where pure x = Now x (Now f) <*> (Now x) = Now (f x) (Later f) <*> x = Later (f <*> x) f <*> (Later x) = Later (f <*> x) instance Monad Partial where return = pure f >>= (Now x) = f x f >>= (Later x) = Later (f x) Partial is so trivial that everything can be made co-recursive by wrapping all function bodies in "Later". All of the "Later" wrappers will get nested together by the Applicative/Monad; everything will "just work". The one missing piece is the following function, which isn't total: runPartial :: Partial a -> a runPartial (Now x) = x runPartial (Later x) = runPartial x We could name it `unsafeForcePartial` and treat it with care, like we currently do with `unsafePerformIO`.
  - throwaway283719 12y ago
    Can you explain how this makes every function total? For example, take the `head` function which is not total head :: [a] -> a head (x:xs) = x head [] = undefined How can you make this total using `Partial`? I can get as far as headTotal :: [a] -> Partial a headTotal (x:xs) = Now x headTotal [] = Later (...) but what goes in (...)?
    - pdpi 12y ago
      This is why it's always seemed to me that head ought to be typed as head :: [a] -> Maybe a