Historically, Hydra has considered the name/term bindings which make up the top-level structure of the graph to be distinct from the name/term bindings found in let-expressions. In LambdaGraph, however, these are the same thing; a graph is essentially just a term which, if it happens to be a let-term, defines elements as its bindings. Type inference in Hydra does not yet reflect this unity, with elements and let-terms being the subject of completely different inference logic.
Along with this change, it may be possible to eliminate the need for user-provided type annotations on (many) mutually recursive elements and mutually recursive let-bindings, as well as the need for topological sorting of elements prior to inference.
joshsh
commented
4 months ago
Historically, Hydra has considered the name/term bindings which make up the top-level structure of the graph to be distinct from the name/term bindings found in let-expressions. In LambdaGraph, however, these are the same thing; a graph is essentially just a term which, if it happens to be a let-term, defines elements as its bindings. Type inference in Hydra does not yet reflect this unity, with elements and let-terms being the subject of completely different inference logic.
Along with this change, it may be possible to eliminate the need for user-provided type annotations on (many) mutually recursive elements and mutually recursive let-bindings, as well as the need for topological sorting of elements prior to inference.
See also #103.