3 ms·
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 t
by 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 agoCan 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 agoThis is why it's always seemed to me that head ought to be typed as head :: [a] -> Maybe a
- NickPollard 12y agoScala's collections have this function as headOption, which I use almost exclusively over head.
- tome 12y agoI guess you need a special definition diverge = Later diverge headTotal [] = diverge
- chriswarbo 12y agoYep, 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".