4 ms·

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

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
    - NickPollard 12y ago
      Scala's collections have this function as headOption, which I use almost exclusively over head.
  - tome 12y ago
    I guess you need a special definition diverge = Later diverge headTotal [] = diverge
    - chriswarbo 12y ago
      Yep, although it doesn't actually diverge; that's the point ;) The classic "loop" function, which is completely polymorphic, does diverge: loop :: a loop = loop "loop" will never return a value, since to perform one 'step', it must perform an 'infinite' amount of computation. The function you've written doesn't diverge, since it will immediately return a value "Later x" after one step. As long as we're using laziness, it doesn't matter that "x" itself is 'infinite': loop' :: Partial a loop' = Later loop' Note that we can do an equivalent thing in strict languages, by eta-expanding our definitions into thunks: data Partial' a = Now a | Later (() -> Partial a) loop'' :: () -> Partial a loop'' _ = Later loop'' We can use "loop :: a" in place of "undefined :: a", since they have the same type. We can't use "loop' :: Partial a" in the same way, since its type is different. "loop' :: Partial a" is a bit like a 'phantom type', where the "a" in its type signature never actually occurs in the value. In fact, we can define a type which doesn't contain "Now", and is thus guaranteed to never terminate: data Inf a = Inf (Inf a) Of course, the "a" in "Inf a" is a true phantom: it doesn't affect the values at all. We can get rid of it to obtain: data Loop = Loop Loop We can use this type to "drive" main loops for servers, operating systems, games, etc. in a total language: server :: Loop -> IO Loop server (Loop x) = do req <- readRequest sendResponse (process req) Loop <$> server x "Loop" is equivalent to "Stream ()", where: data Stream a = Cons a (Stream a) Of course, "Stream a" is to "[a]" what "Inf a" is to "Partial a": it's just missing the base-case ("[]" and "Now a", respectively). Interestingly, we can think of "Partial a" as being like "[a]", except that it stores elements in "[]" rather than ":". Alternatively, we can think of "Partial a" as being like "Nat" (the Peano numbers), which uses an element of "a" in place of "Zero".

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
  - NickPollard 12y ago
    Scala's collections have this function as headOption, which I use almost exclusively over head.
- tome 12y ago
  I guess you need a special definition diverge = Later diverge headTotal [] = diverge
  - chriswarbo 12y ago
    Yep, although it doesn't actually diverge; that's the point ;) The classic "loop" function, which is completely polymorphic, does diverge: loop :: a loop = loop "loop" will never return a value, since to perform one 'step', it must perform an 'infinite' amount of computation. The function you've written doesn't diverge, since it will immediately return a value "Later x" after one step. As long as we're using laziness, it doesn't matter that "x" itself is 'infinite': loop' :: Partial a loop' = Later loop' Note that we can do an equivalent thing in strict languages, by eta-expanding our definitions into thunks: data Partial' a = Now a | Later (() -> Partial a) loop'' :: () -> Partial a loop'' _ = Later loop'' We can use "loop :: a" in place of "undefined :: a", since they have the same type. We can't use "loop' :: Partial a" in the same way, since its type is different. "loop' :: Partial a" is a bit like a 'phantom type', where the "a" in its type signature never actually occurs in the value. In fact, we can define a type which doesn't contain "Now", and is thus guaranteed to never terminate: data Inf a = Inf (Inf a) Of course, the "a" in "Inf a" is a true phantom: it doesn't affect the values at all. We can get rid of it to obtain: data Loop = Loop Loop We can use this type to "drive" main loops for servers, operating systems, games, etc. in a total language: server :: Loop -> IO Loop server (Loop x) = do req <- readRequest sendResponse (process req) Loop <$> server x "Loop" is equivalent to "Stream ()", where: data Stream a = Cons a (Stream a) Of course, "Stream a" is to "[a]" what "Inf a" is to "Partial a": it's just missing the base-case ("[]" and "Now a", respectively). Interestingly, we can think of "Partial a" as being like "[a]", except that it stores elements in "[]" rather than ":". Alternatively, we can think of "Partial a" as being like "Nat" (the Peano numbers), which uses an element of "a" in place of "Zero".