1. 19 Jun, 2022 2 commits
  2. 03 Jun, 2022 1 commit
  3. 24 May, 2022 1 commit
  4. 07 May, 2022 1 commit
    • gilmi's avatar
      Big type inference refactor - add generalize · 2837c73e
      gilmi authored
      We want to be able to infer each term definition group independantly
      from start to finish (elaboration -> solving -> substitution) without
      needing to share the type variable seed between groups, so this
      algorithm can scale up to multiple modules.
      
      For that, we need to add a step after substitution - generalize the
      term definition. We do this by adding a new kind of type:
      
      > TypeScheme [TypeVar] Type
      
      which closes over all of the type variables in the type.
      Consider it similar to a type level lambda that takes types as
      arguments and returns a type which replaces all type variables with
      the respective type arguments.
      
      This simplifies the code because we no longer to distinguish between
      Monomorphic and Polymorphic types, and we only need one Constraint:
      Equality.
      
      Where we used InstanceOf before, we use Equality. If the type on the
      right is a type scheme, we will instantiate it during constraint solving.
      When we encounter a constraint of the form:
      
      > Equality t1 (TypeScheme typevars t2)
      
      We instantiate t2 with fresh arguments replacing the typevars, like we
      did with InstanceOf.
      
      After we finish solving, producing a substitution, and subtituting the
      type variables with their respective types in the substitution, we
      generalize the type of each term definition and close over the type
      variables.
      
      So for example this term definition:
      
      > id x = x
      
      Will have this type after the substitution:
      
      > TypeApp (->) (TypeVar "t1") (TypeVar "t1")
      
      and after the generalization it will have the type:
      
      > TypeScheme ["a"] (TypeApp (->) (TypeVar "a") (TypeVar "a"))
      
      Which will be represented syntactically as:
      
      > id : forall a. a -> a
      2837c73e
  5. 05 May, 2022 1 commit
  6. 06 Apr, 2022 1 commit
  7. 30 Mar, 2022 1 commit
  8. 23 Mar, 2022 1 commit
  9. 23 Jan, 2022 3 commits
  10. 30 Dec, 2021 1 commit
  11. 17 Dec, 2021 2 commits
  12. 08 Dec, 2021 1 commit
  13. 03 Dec, 2021 1 commit
  14. 29 Sep, 2021 1 commit
  15. 06 Jul, 2021 1 commit
  16. 09 May, 2021 2 commits
  17. 28 Apr, 2021 1 commit
  18. 13 Apr, 2021 2 commits
  19. 12 Apr, 2021 3 commits
  20. 11 Apr, 2021 1 commit
  21. 10 Apr, 2021 1 commit
  22. 09 Apr, 2021 1 commit
  23. 08 Apr, 2021 2 commits
  24. 07 Apr, 2021 6 commits
  25. 06 Apr, 2021 2 commits