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.
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