For what it’s worth, unification should not be difficult to implement; a bare-bones unification monad without backtracking should take fewer than 100 lines of Haskell, using the µKanren recipe. The type-checker can then be written as type judgements, taking one or two lines for each production. I say this because I don’t like to think of folks having to maintain thousands of lines of excess compiler infrastructure.
For example, consider that Haskell is terser than RPython. In my implementation of Cammy, it takes 148 lines to implement the µKanren core (sampler/cammylib/types.py) and about another 126 lines to type-check 39 productions (sampler/cammylib/arrows.py), without macros. Haskell is also terser than Scheme. The module implementing relational type-checking (allowing type-driven program synthesis) is 289 lines (movelist/cammyo.scm), of which 133 lines are type-checking and the rest are evaluation.
One frustration I’ve had with using a unification monad is having to open up the datatypes to make room for logic variables.
For example, if my language is:
type Name = String
data Expr = Const Int | Var Name | Lam Name Expr | App Expr Expr
data Type= TInt | TFun TypeType
and I want to use unification, I have to add a case for logic variables:
data Type= TInt | TFun TypeType| TVar LogicVar
which is unsatisfying because LogicVar isn’t part of my language; it’s part of the typechecking machinery.
I’ve also seen this pattern recommended (from unification-fd probably), using open recursion to keep the logic variables separate:
data TypeF a = TInt | TFun a a
typeType= Fix TypeF
type TypecheckerType = UTerm TypeF
but I didn’t really like this either… I think because the Fix wrapper added noise:
-- before
example :: Typeexample= TFun TInt(TFun TInt TInt)
-- after
example :: Typeexample= Fix (TFun (Fix TInt) (Fix (TFun (Fix TInt) (Fix TInt))))
So if avoiding unification means I don’t need a representation for partially-fleshed-out types, that still seems appealing.
What’s your opinion or recommendation on this? For Cammy, maybe it wasn’t a problem because the logic programming is embedded in a dynamically typed language?
This is a great example! It’s relevant to my work too: I have an RPython implementation that I want to make generic, so that other interpreters can use it, but it’s too tightly tied to a single interpreter’s classes.
So, Najd & Peyton Jones call this the “tree decoration problem.” Great name! Their attempt at solving it is called Trees that Grow and there’s a plan for implementing it in GHC. A closely-related problem, the “AST typing problem,” shows up here and has discussion at Lambda The Ultimate, from Yang, and from McKenna; note that we aren’t putting types on ASTs, but putting types on logic variables which are “interpreted” by generic traversals.
I cheat the problem in multiple ways. In RPython for Monte, there are no types; instead, objects guard each other, and are referred to with generic fat pointers to objects. In RPython for Cammy, I hand-wrote a specialized µKanren which only works for Cammy’s type grammar, and I monomorphize when emitting bytecode. In CHICKEN Scheme for Cammy, I take full advantage of CHICKEN’s flexible encoding to intermix logic variables and AST fragments with user-level values.
There’s a related problem, which is how unification interacts with type errors. If you’re doing pure unification, you realize at some arbitrary point in time that a = Maybe Int but also a = Maybe String. Where did these come from? Which one is wrong? If one is from a type signature and the other is from a value, then the type error should be at the location of the value, because it didn’t have the expected type. They could also both be from type signatures, or both from values. How is this provenance information tracked? What do you do when the type mismatch came from a chain of reasoning 7 steps long each at different source locations? What happens when there are higher-kinded types – I don’t even know what questions to ask in that case, but imagine they’re tricksy questions.
I always give type signatures to functions in Haskell, in part to improve the error messages. And I imagine it’s not trivial for its error messages to be as good as they are, given that it’s doing unification.
Yeah, ergonomics is important. For what it’s worth, it should be easy to extend the linked recipe to add annotations to logic variables, such that we get a list of annotations upon (dis)unification; this is like turning the logic monad into a union-find/disjoint-set monad. I haven’t seen anybody actually do this, though.
I think the interesting core here is that if you drop unification you still can express a lot, and it doesn’t prevent you from showing up with unification later.
From a practical perspective it’s a nice trick, I think. Though the microKanren paper looks super interesting, and I’ll definitely be trying to work through it.
IIUC the OP was referring to how the size of a typechecker scales with language size (# of syntactic constructs), rather than the size of a minimal implementation.
I assumed that as well. For comparison, Grace appears to have 15 productions in the concrete syntax, so I would hope that it only takes about 60 lines of code to type-check it; using Pareto-style reasoning, maybe 120 lines at most.
For what it’s worth, unification should not be difficult to implement; a bare-bones unification monad without backtracking should take fewer than 100 lines of Haskell, using the µKanren recipe. The type-checker can then be written as type judgements, taking one or two lines for each production. I say this because I don’t like to think of folks having to maintain thousands of lines of excess compiler infrastructure.
For example, consider that Haskell is terser than RPython. In my implementation of Cammy, it takes 148 lines to implement the µKanren core (
sampler/cammylib/types.py) and about another 126 lines to type-check 39 productions (sampler/cammylib/arrows.py), without macros. Haskell is also terser than Scheme. The module implementing relational type-checking (allowing type-driven program synthesis) is 289 lines (movelist/cammyo.scm), of which 133 lines are type-checking and the rest are evaluation.score 10 · canonical
One frustration I’ve had with using a unification monad is having to open up the datatypes to make room for logic variables.
For example, if my language is:
type Name = String data Expr = Const Int | Var Name | Lam Name Expr | App Expr Expr data Type = TInt | TFun Type Typeand I want to use unification, I have to add a case for logic variables:
data Type = TInt | TFun Type Type | TVar LogicVarwhich is unsatisfying because
LogicVarisn’t part of my language; it’s part of the typechecking machinery.I’ve also seen this pattern recommended (from unification-fd probably), using open recursion to keep the logic variables separate:
data TypeF a = TInt | TFun a a type Type = Fix TypeF type TypecheckerType = UTerm TypeFbut I didn’t really like this either… I think because the
Fixwrapper added noise:-- before example :: Type example = TFun TInt (TFun TInt TInt) -- after example :: Type example = Fix (TFun (Fix TInt) (Fix (TFun (Fix TInt) (Fix TInt))))So if avoiding unification means I don’t need a representation for partially-fleshed-out types, that still seems appealing.
What’s your opinion or recommendation on this? For Cammy, maybe it wasn’t a problem because the logic programming is embedded in a dynamically typed language?
score 3 · canonical
This is a great example! It’s relevant to my work too: I have an RPython implementation that I want to make generic, so that other interpreters can use it, but it’s too tightly tied to a single interpreter’s classes.
So, Najd & Peyton Jones call this the “tree decoration problem.” Great name! Their attempt at solving it is called Trees that Grow and there’s a plan for implementing it in GHC. A closely-related problem, the “AST typing problem,” shows up here and has discussion at Lambda The Ultimate, from Yang, and from McKenna; note that we aren’t putting types on ASTs, but putting types on logic variables which are “interpreted” by generic traversals.
I cheat the problem in multiple ways. In RPython for Monte, there are no types; instead, objects guard each other, and are referred to with generic fat pointers to objects. In RPython for Cammy, I hand-wrote a specialized µKanren which only works for Cammy’s type grammar, and I monomorphize when emitting bytecode. In CHICKEN Scheme for Cammy, I take full advantage of CHICKEN’s flexible encoding to intermix logic variables and AST fragments with user-level values.
score 3 · canonical
There’s a related problem, which is how unification interacts with type errors. If you’re doing pure unification, you realize at some arbitrary point in time that
a = Maybe Intbut alsoa = Maybe String. Where did these come from? Which one is wrong? If one is from a type signature and the other is from a value, then the type error should be at the location of the value, because it didn’t have the expected type. They could also both be from type signatures, or both from values. How is this provenance information tracked? What do you do when the type mismatch came from a chain of reasoning 7 steps long each at different source locations? What happens when there are higher-kinded types – I don’t even know what questions to ask in that case, but imagine they’re tricksy questions.I always give type signatures to functions in Haskell, in part to improve the error messages. And I imagine it’s not trivial for its error messages to be as good as they are, given that it’s doing unification.
score 8 · canonical
Yeah, ergonomics is important. For what it’s worth, it should be easy to extend the linked recipe to add annotations to logic variables, such that we get a list of annotations upon (dis)unification; this is like turning the logic monad into a union-find/disjoint-set monad. I haven’t seen anybody actually do this, though.
score 3 · canonical
I think the interesting core here is that if you drop unification you still can express a lot, and it doesn’t prevent you from showing up with unification later.
From a practical perspective it’s a nice trick, I think. Though the microKanren paper looks super interesting, and I’ll definitely be trying to work through it.
score 2 · canonical
IIUC the OP was referring to how the size of a typechecker scales with language size (# of syntactic constructs), rather than the size of a minimal implementation.
score 1 · canonical
I assumed that as well. For comparison, Grace appears to have 15 productions in the concrete syntax, so I would hope that it only takes about 60 lines of code to type-check it; using Pareto-style reasoning, maybe 120 lines at most.
score 1 · canonical