4 ms·
> As agda is total, and requires everything be proved to halt. Not quite; everything in Agda must either terminate or co-terminate. We can use co-termination t
by chriswarbo 4y ago
> As agda is total, and requires everything be proved to halt.
Not quite; everything in Agda must either terminate or co-terminate. We can use co-termination to represent general recursion, e.g. using Delay:
data Delay : Type -> Type where
Now : {t: Type} -> t -> Delay t
Later : {t: Type} -> Delay t -> Delay t
It's trivial to write any program using Delay, e.g. if we have a function 'step: TuringMachine -> TuringMachine' which performs one step of any Turing machine, we can run any TuringMachine using:
run : TuringMachine -> Delay TuringMachine
run thisState = case thisState == nextState of
true -> Now thisState -- We've entered a halting state
false -> Later (run nextState)
where nextState = step thisState
This is similar to "infinite lists" in lazy languages (like Haskell); e.g. if we call 'run' with a non-halting TuringMachine, we'll get 'Later (Later (Later (...)))'
- cvoss 4y agoBut I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call to 'step' and then terminates with the result 'Later <an unevaluated expression>'. Further computation only occurs if and when you pump the 'Later ...' value for further terms, and that can happen only finitely many times because repeated pumping can only come from a standard recursion, ultimately, which is terminating.
- SkySkimmer 4y agoDid HN eat the delay symbol? I don't think a regular "data" would work for this. https://agda.readthedocs.io/en/v2.6.3/language/coinduction.html#old-coinduction https://agda.readthedocs.io/en/v2.6.3/language/coinduction.h...
- chriswarbo 4y agoOops, yeah; I know Agda needs special handling for codata (co-patterns, sharp/flat, etc.) Ironically, I'm more familiar with using codata in Coq; even though it's notoriously under-supported (breaking subject-reduction, no alternative to cofix, etc.)
- deleted 4y ago[deleted]
- hgsgm 4y agoLists have a consumable head. What you constructed looks like a left fold, a stack of wrappers with the data buried at the bottom.
- chriswarbo 4y ago> a stack of wrappers with the data buried at the bottom Yes, 'Delay t' stores a value "at the end" (in the 'Now' constructor), but doesn't store anything "on the way" (in the 'Later' constructor). In contrast, 'List t' stores values "on the way" (in Cons), but doesn't store anything "at the end" (in Nil). Another useful example is (Peano) natural numbers, which don't store any values "at the end" (Zero) or "on the way" (Successor). Natural numbers are isomorphic to 'List ()' and 'Delay ()' (whose 'elements' contain no information) > Lists have a consumable head Slight nit-pick: only non-empty lists have a head. Non-empty lists are isomorphic to '(t, List t)'. Consuming the head of a 'Delay t' is still useful, since they act like a counter; or (equivalently) as a notion of logical time. I find this stuff fascinating, and explored it in more detail at http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.htm...