wisnesky
commented
1 year ago 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 https://github.com/CategoricalData/hydra/issues/90, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA2QKN5UJO3F2UHPCFMNT23XK5CNTANCNFSM6AAAAAAZDU5G64. You are receiving this because you were mentioned.
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.