Investigate support for coinductive types

[joshsh]

Ryan said some mumbo jumbo once about general-purpose support for coinductive types, as in Coq and Charity. Look into this. Hydra has some superficial support for stream types, but this support has not made its way into the Lambda Graph spec, nor are streams currently being used for any applications of Hydra. It would be nice to fold support for streams and other coinductive types into the data model at a fundamental level. It is acceptable that terms of these types may not translate easily and automatically into the host languages (Haskell and Java), so long as they are useful for applications.

[joshsh]

Possibly related musings from @wisnesky :

something i've been wondering about for a while is if there is a connection between your graphs and the fact that a parametric model of system F is a reflexive graph
Image
Image
joshsh — Today at 10:18 AM
Bunch of unfamiliar terms there. What are reflexive graphs?
wisnesky — Today at 10:18 AM
graphs with self edges
https://ncatlab.org/nlab/show/reflexive+graph
joshsh — Today at 10:20 AM
Self-edges are allowed, but it is not the case that every vertex has a self-edge
wisnesky — Today at 10:21 AM
right, i doubt your idea is exactly the same thing
joshsh — Today at 10:23 AM
If you can illustrate what consequences your idea would have, there is always space for another GitHub issue
wisnesky — Today at 10:24 AM
these graph models of system F prove more equations than just the axioms of system F
joshsh — Today at 10:24 AM
I see (sorta)
wisnesky — Today at 10:24 AM
for example, plain F can't prove that /\x \y:x x is the only inhabitant of "forall x, x->x", but the graph models do
anyway, for that reason, actual implementations of F will sometimes be based on the more specific models
like, HoTT Coq works that way
https://bentnib.org/dtt-parametricity.html
so if you had a system F implementation based on reflexive graph models, it would already have e.g. inductive types. where plain F only has weak inductive types (see here https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt)

[wisnesky]

Here you go, System F with existential types gets you coinduction: https://www.andrew.cmu.edu/course/15-312/recitations/rec6-notes.pdf

…

On Jun 12, 2023, at 10:28 AM, Joshua Shinavier ***@***.***> wrote: Possibly related musings from @wisnesky <https://github.com/wisnesky> : something i've been wondering about for a while is if there is a connection between your graphs and the fact that a parametric model of system F is a reflexive graph Image Image joshsh — Today at 10:18 AM Bunch of unfamiliar terms there. What are reflexive graphs? wisnesky — Today at 10:18 AM graphs with self edges https://ncatlab.org/nlab/show/reflexive+graph joshsh — Today at 10:20 AM Self-edges are allowed, but it is not the case that every vertex has a self-edge wisnesky — Today at 10:21 AM right, i doubt your idea is exactly the same thing joshsh — Today at 10:23 AM If you can illustrate what consequences your idea would have, there is always space for another GitHub issue wisnesky — Today at 10:24 AM these graph models of system F prove more equations than just the axioms of system F joshsh — Today at 10:24 AM I see (sorta) wisnesky — Today at 10:24 AM for example, plain F can't prove that /\x \y:x x is the only inhabitant of "forall x, x->x", but the graph models do anyway, for that reason, actual implementations of F will sometimes be based on the more specific models like, HoTT Coq works that way https://bentnib.org/dtt-parametricity.html so if you had a system F implementation based on reflexive graph models, it would already have e.g. inductive types. where plain F only has weak inductive types (see here https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt) — Reply to this email directly, view it on GitHub <#88 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN7M7UBG6Q2PIB7R24TXK5GVPANCNFSM6AAAAAAZDT4LA4>. You are receiving this because you were mentioned.