(As usual in the discussion of problems of this kind, it's better to talk about mathematically specific programming languages/type theories instead of Haskell/OCaml/Agda.)
In call-by-value languages, for every type τ, we actually have two different things in the language: (1) values of type τ and (2) computations of type τ. Only values can substitute variables of type τ, and if the language has recursion (or some computational effects), only computations support recursion/effects. Now coming back to inductive data types, because general recursion is not allowed on values, so we don't have to (and shouldn't) include infinite values as _values_ of inductive types. General recursion only forces us to include infinite/divergent computations as _computations_ of inductive types. We can of course separately have coinductive types, whose _values_ have infinite values.
Paul Levy's work on call-by-push-value answers questions like this extremely clearly. I highly recommend checking out the first chapters of this CBPV book. (A while ago I think I saw on mastodon that someone said CBPV isn't about computational effects. I was quite surprised because CBPV is totally about computational effects...)
Zhixuan Yang
npub1v6…ac7s4
2025-04-27 17:44:48 UTC
in reply to nevent1q…23hh
Author Public Key
npub1v6afl9hlcsdeqcw06j3lqtv48xjqpmfyp2nc5e6k829vlp5ekg3qjac7s4Seen on
wss://relay.momostr.pinkPublished at
2025-04-27 17:44:48 UTCEvent JSON
{
"id": "d302d7bc3666bea702c52ad07a983ea18157ce12f699045a332e258a80f16cca",
"pubkey": "66ba9f96ffc41b9061cfd4a3f02d9539a400ed240aa78a67563a8acf8699b222",
"created_at": 1745775888,
"kind": 1,
"tags": [
[
"e",
"e280235aba917f6c084e0228693a48f0a067cb4f301d71e543237086549005d4",
"",
"reply",
"e613f8d3f4092d399e5125d1704bf2dffe686f6b92116e1921e78ea9cc6993dc"
],
[
"p",
"ad31a78bd2c38886e959e72a18f79d3b188f45ccad0d1d8c2e1e9f3857b40add"
],
[
"proxy",
"https://mathstodon.xyz/@zyang/114411168608167850",
"web"
],
[
"e",
"9a6397b7126625b66e5cf9d64d801a469b07adb9c7c41988d89efb01f527b9eb",
"",
"root",
"e613f8d3f4092d399e5125d1704bf2dffe686f6b92116e1921e78ea9cc6993dc"
],
[
"p",
"e613f8d3f4092d399e5125d1704bf2dffe686f6b92116e1921e78ea9cc6993dc"
],
[
"proxy",
"https://mathstodon.xyz/users/zyang/statuses/114411168608167850",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/zyang/statuses/114411168608167850",
"pink.momostr"
],
[
"-"
]
],
"content": "(As usual in the discussion of problems of this kind, it's better to talk about mathematically specific programming languages/type theories instead of Haskell/OCaml/Agda.)\n\nIn call-by-value languages, for every type τ, we actually have two different things in the language: (1) values of type τ and (2) computations of type τ. Only values can substitute variables of type τ, and if the language has recursion (or some computational effects), only computations support recursion/effects. Now coming back to inductive data types, because general recursion is not allowed on values, so we don't have to (and shouldn't) include infinite values as _values_ of inductive types. General recursion only forces us to include infinite/divergent computations as _computations_ of inductive types. We can of course separately have coinductive types, whose _values_ have infinite values.\n\nPaul Levy's work on call-by-push-value answers questions like this extremely clearly. I highly recommend checking out the first chapters of this CBPV book. (A while ago I think I saw on mastodon that someone said CBPV isn't about computational effects. I was quite surprised because CBPV is totally about computational effects...)",
"sig": "1ef4fc3184025b6283e4ddabeba37c53a2c345454363928e75dd135fdb1f68a2dd1d8bc301f7bbc0f45bd960845d9b46bcc35379c0d599b729d0af31b8e47290"
}