Mostly “functional”-style, in the sense of having algebraic data types and expressions as the chief syntactic construct, but with this system of subtyping and objects for the things like modules and closure types that actually need the existential type. I ended up writing my own type-inference algorithm, which I’m still formalizing in Coq now.
Mostly “functional”-style, in the sense of having algebraic data types and expressions as the chief syntactic construct, but with this system of subtyping and objects for the things like modules and closure types that actually need the existential type. I ended up writing my own type-inference algorithm, which I’m still formalizing in Coq now.
Rabbit. Hole.
Sounds like loads of fun :)