Support type inference for recursive elements

[joshsh]

Hydra's formal data model (Lambda Graph) includes a variant of Hindley-Milner type inference which has been adapted slightly for nominal types (records, unions, and wrappers). However, while λG conceives of graphs as mutually recursive let terms and technically permits any graph which can be typed, its type inference does not extend to let terms with actual recursion -- instead, it relies on type annotations to provide the expected type, which are then simply checked for consistency. Ideally, λG would dispense with user-provided type annotations altogether, and simply disallow terms for which type inference fails. That would require a refinement of λG type inference which can in fact deal with recursion. This is to be investigated. @wisnesky has suggested HMX (reference?) constraint-based methods as an alternative to Algorithm W in Hydra.

[wisnesky]

Here is the HMX reference http://www.cs.cmu.edu/~aleksey/talks/refinements03/hmx.pdf

…

On Jun 12, 2023, at 9:52 AM, Joshua Shinavier ***@***.***> wrote: Hydra's formal data model (Lambda Graph) includes a variant of Hindley-Milner type inference which has been adapted slightly for nominal types (records, unions, and wrappers). However, while λG conceives of graphs as mutually recursive let terms and technically permits any graph can be typed, its type inference does not extend to let terms with actual recursion -- instead, it relies on type annotations to provide the expected type, which are then simply checked for consistency. Ideally, λG would dispense with user-provided type annotations altogether, and simply disallow terms for which type inference fails. That would require a refinement of λG type inference which can in fact deal with recursion. This is to be investigate. @wisnesky <https://github.com/wisnesky> has suggested HMX (reference?) constraint-based methods as an alternative to Algorithm W in Hydra. — Reply to this email directly, view it on GitHub <#90>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN5UJO3F2UHPCFMNT23XK5CNTANCNFSM6AAAAAAZDU5G64>. You are receiving this because you were mentioned.

[joshsh]

Two other links from @wisnesky: this'n and this'n. Apparently, one should just be able to bind the let keys to type variables and let unification do its thing.

[wisnesky]

Yup, there’s the problem, someone set this thing to “evil”. https://www.youtube.com/watch?v=Y8dcmLscf3g

…

On Jul 14, 2023, at 8:30 PM, Joshua Shinavier ***@***.***> wrote: Two other links from @wisnesky <https://github.com/wisnesky>: this'n <https://stackoverflow.com/questions/49134312/hindley-milner-type-inference-for-mutually-recursive-functions> and this'n <https://stackoverflow.com/questions/67254536/how-can-i-infer-types-for-recursive-functions>. Apparently, one should just be able to bind the let keys to variables and let unification do its thing. — Reply to this email directly, view it on GitHub <#90 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA2QKN7S7UOZFLTLGV4F5BDXQIFHBANCNFSM6AAAAAAZDU5G64>. You are receiving this because you were mentioned.