Posted because this feature in particular sounded cool:

GB also packs functionality for complexity analysis.

Although, it’s a little different from what I thought. I was imagining you give it a function and a range of input sizes, and it returns one of O(1), O(log n), O(n), O(n log n) … etc, whichever seems to fit best. Instead it looks like you have to tell it “this is O(n log n)” and it tells you which constant factor fits that curve best. But it does also tell you the (root-mean-square) error, so I guess you’d use this to check how well it fits the curve you expect.

score 2 · 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 Type

and I want to use unification, I have to add a case for logic variables:

data Type = TInt | TFun Type Type | 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
type Type = Fix TypeF
type TypecheckerType = UTerm TypeF

but I didn’t really like this either… I think because the Fix wrapper 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

Union finds can be implemented in different styles. An arena style or a refcell/pointer style.

What’s an “arena-style union find”? Is that where you use a separate dictionary that maps from node ID to the representative ID of its equivalence class? I guess that’s like an area in that you can control when that dictionary is freed.

score 2 · canonical