3 ms·
Total means that the function must always return a value. In the presence of coinductive types and corecursive functions, a total function can run forever but m
by bidirectional 5y ago
Total means that the function must always return a value. In the presence of coinductive types and corecursive functions, a total function can run forever but must always be producing values when asked. e.g. an infinite stream of prime numbers can be produced by a corecursive, total function. You can use this to embed Turing complete computations in languages like Agda or Coq[1], they just must be declared as such up front. Much like IO must be declared up front in (idiomatic) Haskell. And much like you can unsafePerformIO in Haskell, Idris and Agda have their own escape hatches as the sibling comment mentions.
[1] https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T...
- sadfev 5y agoThanks for clarifying, I haven’t studied co-inductive types yet.
- throwaway17_17 5y agoI have heard multiple authors and speakers (while watching various lectures and in papers) say emphatically that no one wants to deal with coinductiion in a type theory unless they ABSOLUTELY must. I'm not sure I've ever seen a concise explanation of the complications that arise by inserting coinductive types into a type theory, but I'll take it as an article of faith that the issues exist. But, the concept is certainly intriguing. Somehow, in my reading on type theory there has been a lack of exploration of instantiation of coinductive types, hopefully the paper by McBride you linked will give me some references to chase down.