2 ms·
Yep, although it doesn't actually diverge; that's the point ;) The classic "loop" function, which is completely polymorphic, does diverge: loop :: a l
by 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".