4 ms·

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

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".

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".