~icefox/rust-bidi

Experiment in implementing bidirectional type checking. Based on https://arxiv.org/pdf/1306.6032.pdf

There's two key parts, check(e, A, ctx) that takes type A as an input and defines that the term e checks against that type under the given judgement, and synthesis(e, A, ctx) which takes the term e and produces a type A.

Without polymorphism, the rule for checking application e1(e2) is to synthesize type A -> B for e1, and then check e2 against A. This works for simple expressions but not polymorphism since we want to synthesize a generic type 'a -> 'b for e1 and then we don't have anything useful to check e1 against.

So they add a third rule, application(e, A, C, ctx) which says "under context ctx, applying a function of type A to term e synthesizes type C."

References:

https://github.com/nikomatsakis/bidir-type-infer
https://github.com/ThePuzzlemaker/sysf-rs (new-dunfield2013 branch) (Thank you @Paradoxical)
https://github.com/lexi-lambda/higher-rank/blob/master/library/Language/HigherRank/Typecheck.hs (this turned out to be the most difficult one to get a grip on but also the best one once you've read the paper a couple times)

MBones — Today at 11:06 PM
uvar is unification var prolly
this is something that really bugs be tbh, there's like 17 names for this one thing
and half of them make no sense

icefox — Today at 11:07 PM
evar is existential var, maybe?

MBones — Today at 11:07 PM
that'd be my guess

icefox — Today at 11:08 PM
neither of those names really tell me much

MBones — Today at 11:09 PM
unification variable, existential variable, logic variable, just "variable", metavariable, and finally (my least favorite one) "constant"

MBones — Today at 11:11 PM
are you familiar with the basic ideas of type inference via unification?

icefox — Today at 11:11 PM
ssssssssorta.

icefox — Today at 11:13 PM
I've done basic HM type inference, though not well.

icefox — Today at 11:13 PM
It seemed to be "collect all the facts you can about your types, then step through each fact recursively evaluating all the unknowns until either you're out of out of unknowns and you have a real type, or you're out of knowns and the typechecking fails."
the main point being that you don't "look ahead" or "look behind" in the program to find more facts, you just find everything you can and consider it all at once.

MBones — Today at 11:15 PM
so with type inference via unification, instead of taking two complete types and checking that they're equal, you take two types with holes in them and try to fill in the holes so that they're equal (unification)
and hopefully by the time you're done checking a function, all the holes have been filled in
the holes are called unification variables (among other (mostly worse) names)

icefox — Today at 11:19 PM
wow that actually makes sense
please teach me more oh sage

MBones — Today at 11:20 PM
iirc in the "complete and easy" paper, the holes are more complicated than normal, since not every hole can be filled with every type

icefox — Today at 11:22 PM
hmmmm

"%{{author m9_macro}}" — Today at 11:26 PM
Sounds easier to chuck all the constraints into a logic solver and let the solver deal with figuring stuff out

MBones — Today at 11:26 PM
you have to keep track of the "scope" of the hole so that filling it in doesn't accidentally make types with scope errors -- like, in the type (forall s. s -> A) -> A where A is a hole, you can't fill A with s since that would result in (forall s. s -> s) -> s, which doesn't make sense

MBones — Today at 11:29 PM
Usually, the logic solver is simple enough (only a unify method) that you can write it yourself with only a few lines of code! Have you seen zesterer's type inference in 100 lines?

"%{{author m9_macro}}" — Today at 11:29 PM
Fair enough

icefox — Today at 11:30 PM
yeah this logic solver is more complicated but still like, 1000 lines of code
if I can wrap my brain around wtf is going on
and if the example code I'm going from is a good approximation of what the paper actually means, 'cause I can figure out the math but it takes like 10 times longe

#![deny(good_code)] — Today at 11:50 PM
in my implementation UVar is "universal type variable"
afaik that's what uvar in the paper is

#![feature(bad_code, calypso)] — 12/09/2021
you don't need full system Fω
you just need System F extended with type constructors and data constructors — opaque term-level and type-level constants
there was a paper about typeclasses with this, one sec
https://www.cs.tufts.edu/comp/150GIT/archive/mark-jones/fpca93.pdf
ML-based, but similar

(more info at https://www.youtube.com/watch?v=6mvpkvPYf0Y

MBones — 11/20/2021
Here's the code I was worried about:
if something then id else (fun x => x + 1)
here's the difference btw lazy and eager instantiation:
infer term = case term of
  ...
  Var name -> do
  ty <- lookupTypeOfVar name
    -- lazy instantiation:
    return ty
    -- eager instantiation:
    instantiateForalls ty
in eager instantiation, when a variable has a forall type, you instantiate that forall with a fresh unification variable as soon as you see it

heads

clone