Timeline for Coinduction for all?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 16, 2021 at 19:29 | comment | added | Andrej Bauer | Anything might happen. My intention was to let you know about somewhat standard terminology in PL because you used the term "programming language". But now this conversation is past the point of diminishing returns, we should just have a tea. | |
| Nov 16, 2021 at 18:01 | comment | added | Mike Shulman | @AndrejBauer Sure, but I think I am justified in saying that even a "programming language" might be implemented in such a way that normalization occurs under binders. | |
| Nov 16, 2021 at 7:41 | comment | added | Andrej Bauer | And the problem you see is not the only one. In order to make a programming language with dependent types, one also has to figure out what to do with computational effects – saying just "why don't you use a monad?" is a poor answer. | |
| Nov 16, 2021 at 7:38 | comment | added | Andrej Bauer | Yes, typechecking in general requires one to decide equality of open terms, and a common way of doing that is normalization. But I would advise against equating normalization with execution. Execution is a much more general notion which need not be carried out as normalization, at all. How to make a programming language (as opposed to an equational caclulus) out of dependent type theory is currently still not so clear. | |
| Nov 15, 2021 at 21:07 | comment | added | Mike Shulman | @AndrejBauer Yes, I know! My point is that in order to typecheck such a language, one has (I believe) to normalize under binders. So it doesn't seem to me that the phrase "programming language" can be restricted to cases in which only closed programs are executed. | |
| Nov 15, 2021 at 16:54 | vote | accept | user984603 | ||
| Nov 15, 2021 at 16:12 | comment | added | Andrej Bauer | An example of a dependently typed langauge is Idris, and Haskell has been gettting ever more dependent-type features. Usually the emphasis in these languages is on automating as much as possible, for instance propositional assertions might be passed to an automated prover. There's also the question of how to generate code that doesn't contain useless and trivial stuff (such as computing an element of a proposition). And almost always there's an escape hatch of the sort "just trust me". | |
| Nov 15, 2021 at 15:49 | comment | added | Mike Shulman | @AndrejBauer Is it possible, then, to have a dependently typed programming language? Typechecking dependent types in practice requires normalization under binders, no? | |
| Nov 15, 2021 at 1:04 | history | edited | user44143 | CC BY-SA 4.0 |
added link
|
| Nov 14, 2021 at 21:01 | comment | added | Andrej Bauer | Just a small technical remark to an otherwise very illuminating answer: a programming language cannot encounter a variable or an axiom, because only closed programs are ever executed (and there are no axioms). That at least is how I understand the PL canon. | |
| Nov 14, 2021 at 20:56 | comment | added | Andrej Bauer | @MircoA.Mannucci: you might like ellerman.org/the-existence-information-duality | |
| Nov 14, 2021 at 19:23 | comment | added | Mirco A. Mannucci | Then there is constructive math, where poor humans try to "build structures all the way up", for instance N, via induction schema. Then there is another math, still beyond our horizon, which I would call DESTRUCTIVISM, which starts from the opposite perspective: you begin with a static structure, generally infinite, and then proceed by EROSION, moving down the food chain. This math, of which there are already a few scanty examples, would leverage co-inductive methods... | |
| Nov 14, 2021 at 19:23 | comment | added | Mirco A. Mannucci | Great answer. However, reading your finale, I could not refrain from this crazy thought: there is classical mathematics, ie the mathematics from the point of view of God, where structures are God-given, static structures | |
| Nov 14, 2021 at 16:48 | history | answered | Mike Shulman | CC BY-SA 4.0 |