ollef/bidirectional

Haskell implementation of Dunfield and Krishnaswami's "Complete and easy bidirectional typechecking for higher-rank polymorphism"

bidirectional's Issues

Is this the whole of "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism"?

Your implementation is very short!!
I'm going to study it and your code over the christmas break.

is the alpha-conversion in instantiation really necessary (InstLAIIR)?

Hi,

I'm currently implementing these algorithms, in ... Go, of all languages, and the results are as you'd expect. Having your work as a guide is extremely useful. Thank you.

In your implementation, you do alpha-conversion of \beta as part of InstLAIIR. The text doesn't make mention that this is necessary (though I can completely believe this was something that got cut to make a page limit). Did you come across cases where this is essential?

Does not subsume Hindley-Milner?

When trying:

(\x y -> x) ()

I got:

(TFun (TExists (TypeVar "'k")) TUnit,[CExistsSolved (TypeVar "'l") TUnit,CExists (TypeVar "'k")])

This is an invalid type since there is an unsolved existential. Which means typechecking fails for this short program, this doesn't seem right to me,

EDIT: 1s after posting this I realized that the same thing happens in Hindley-Milner, you have to re-generalize after application I guess.

"The impossible happened!"

Attempting to synthesize a type of (λx. x x) fails for obvious reasons, but attempting to synthesize the type with a type annotation -- λx. (x : ∀ a. a → a) x -- produces a "The impossible has happened!" error. Consider the following ghci session:

*Main> let ty = polytype $ TForall (TypeVar "a") (TFun (tvar "a") (tvar "a"))
*Main> run (EAbs x (EApp (EAnno (EVar x) ty) (EVar x)))
"typesynth([], λx. (x : ∀ a. a → a) x)
   typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], ($a : ∀ a. a → a) $a, ∃ 'b)
      typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], ($a : ∀ a. a → a) $a)
         typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], $a : ∀ a. a → a)
            typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a], $a, ∀ a. a → a)
               typecheck([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], $a, 'c → 'c)
                  typesynth([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], $a)
                  =(∃ 'a, [▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c])
                  subtype([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], ∃ 'a, 'c → 'c)
                     instantiateL([▶ 'a, ∃ 'a, ∃ 'b, $a : ∃ 'a, 'c], 'a, 'c → 'c)
                        instantiateR([▶ 'a, ∃ 'e, ∃ 'd, ∃ 'a = ∃ 'd → ∃ 'e, ∃ 'b, $a : ∃ 'a, 'c], 'c, 'd)
*** Exception: The impossible happened! instantiateR: ([▶ 'a, ∃ 'e, ∃ 'd, ∃ 'a = ∃ 'd → ∃ 'e, ∃ 'b, $a : ∃ 'a, 'c], 'c, 'd)
*Main> 

where run is defined in a file Main.hs as follows:

module Main where

import AST
import Context
import NameGen
import Pretty
import Type

import Control.Monad.State

run :: Expr -> String
run e = case runState (typesynth (context []) e) initialNameState of
  (context, _) -> pretty context

How to extend with type applications

Do you have any idea how to extend the system with type applications. I don't know how to extend the subtyping relation, because in general I don't know whether to compare the type applications covariantly or contravariantly. Is the only solution to fall back to unification (unifying foralls using alpha equality)?