Hydra's type inference implementation started with the minimal Algorithm W implementation in Stephen Diehl's "Write You a Haskell", then diverged heavily in order to accommodate the idiosyncrasies of Hydra, including the need for let polymorphism and mutual recursion, as well as syntax features like records and variants. Hydra's inference rules follow the LambdaGraph specification, which is just an extension of the usual Hindley-Milner inference rules for nominal types (again, records, variants, newtypes). The implementation is sufficient for generating all of Hydra's kernel into Haskell and Java, but the implementation is nonstandard, and is need of formal verification.
As an exercise, @wisnesky has written a small Algorithm W implementation from scratch. Let's see if this can evolve into a proof-of-concept which meets Hydra's requirements, then we can compare it with the existing inference implementation. The main missing pieces are likely to be the features mentioned above: support for nominal types (probably not hard) and mutual recursion (the main thing to be demonstrated, IMO). I would also add support for list terms and one or two types of literal terms, as well.
joshsh
commented
5 months ago
Hydra's type inference implementation started with the minimal Algorithm W implementation in Stephen Diehl's "Write You a Haskell", then diverged heavily in order to accommodate the idiosyncrasies of Hydra, including the need for let polymorphism and mutual recursion, as well as syntax features like records and variants. Hydra's inference rules follow the LambdaGraph specification, which is just an extension of the usual Hindley-Milner inference rules for nominal types (again, records, variants, newtypes). The implementation is sufficient for generating all of Hydra's kernel into Haskell and Java, but the implementation is nonstandard, and is need of formal verification.
As an exercise, @wisnesky has written a small Algorithm W implementation from scratch. Let's see if this can evolve into a proof-of-concept which meets Hydra's requirements, then we can compare it with the existing inference implementation. The main missing pieces are likely to be the features mentioned above: support for nominal types (probably not hard) and mutual recursion (the main thing to be demonstrated, IMO). I would also add support for list terms and one or two types of literal terms, as well.