1. 04 Nov, 2020 3 commits
  2. 02 Nov, 2020 9 commits
  3. 01 Nov, 2020 18 commits
  4. 01 Oct, 2020 1 commit
  5. 14 Jul, 2020 3 commits
  6. 01 Jul, 2020 1 commit
    • Gabriel Scherer's avatar
      SolverSig: use an abstract type for O.tyvar · 86503790
      Gabriel Scherer authored
      Currently the Output module signature used by SolverHi lets user provide
      their own `ty` type to represent elaborated types, but it defines
          type tyvar = int
      to directly inject solver-generated inference variable identifier as
      There is a difference in abstraction level here: a signature such as
      `mu : tyvar -> ty -> ty` has a first parameter that is a low-level
      type fixed by the solver, and the second parameter that is
      a user-determined abstract type.
      This lack of abstraction for type variables is problematic for users
      that would want to generate elaborated types on their own, without
      going through inference variables. For example, consider
      language-level support for parametrized type abbreviations:
          type 'a cps = { run : 'r . ('a -> 'r) -> 'r }
      If we want to reflect a user annotation of the form `foo cps` into
      a System F type `∀r. (〚foo〛→r)→r`, we need to generate a Forall
      quantifier for `'r`. But how would the user pick a "fresh" nominal
      variable that is guaranteed to be distinct from those generated by the
      solver ?  (There may be inference variables in scope used in `foo`).
      Currently it is not possible for the user to generate System F binders
      that are guaranteed to be free of conflicts with solver-generated
      variables. The simple change in this commit makes this possible by
      making the `tyvar` type abstract, with an explicit conversion function
      between unique integers and user type variables.
      This enables several possible strategies for users to implement
      a `fresh_tyvar : unit -> tyvar` on the side, that does not conflict
      with `solver_tyvar`. For example:
      1. keep `tyvar = int` but store already-used identifiers in
         a hashtable that is used to provide a conflict-avoiding translation
         in `solver_tyvar.
      2. use even numbers for solver variables and odd numbers for user
      3. use `type tyvar = Solver of int | User of ...`
      We *could* use approaches (1) and (2) above without the separation
      (with the conversion done purely on the client side), but we believe
      that enforcing the separation in the Output signature is the better
      design. It forces users to give a thought to their tyvar
      representation (it's easy to just use `int` and the identity), so they
      will know where to go change things if the need for user-side fresh
      variables arises. Without this API-level guidance, worse solution
      would be considered (our first idea when hitting this issue was to
      expose Inferno's fresh-identifier generator to clients).
  7. 16 Jun, 2020 5 commits