Understanding PureScript typechecking

[klntsky]

This thread is for questions/notes we make while trying to understand the typechecker code

[klntsky]

1. What is the role of TUnknown?

[klntsky]

Looks like a unification variable

[klntsky]

Reposting @gnumonik from Slack for context

• Language.PureScript.AST.* - This stuff is the "initial" fully-sugared AST. This has (e.g.) do notation. Most of what you actually need to look at here is in Language.PureScript.AST.Declarations or the modules under the Declarations namespace.
• Language.PureScript.TypeChecker.Monad defines the typechecking monad, it's state type, and a bunch of functions for manipulating the state of the typechecker. We use the typechecker monad to convert to typed CoreFn (even though we're not strictly checking anything). Of particular note are the functions for binding names & type synonyms, e.g. bindLocalVariables / bindLocalTypeVariables / withScopedTypedVariables etc.
• Language.PureScript.TypeChecker.Types contains the implementation of their type checking and inference machinery. Unfortunately this is a huge and very poorly documented module. We primarily use infer, and the structure of our CoreFn conversion functions tends to follow the structure of the infer/infer' functions there. typesOf is particularly useful, as this lets us infer types correctly for mutually recursive bindings.
◦ Note that we don't use anything (and shouldn't need to use anything) from the Language.PureScript.TypeChecker module itself, as we operate on an already checked AST and only care about deducing/inferring the types for all expressions in the AST
• We shouldn't need to use any other modules from the TypeChecker namespace. They're mostly internal utilities that we don't want to change.
• Language.PureScript.Types defines the types for... types and provides various utilities for working with them. Just like Plutus uses the same types for PIR and UPLC, PureScript uses the same types for both the Language.PureScript.AST syntax tree and the CoreFn syntax tree. We'll have to provide a mapping from PS types to PIR types (though we can assume that there are no free type variables, which will allow us to e.g. transform row-records into products and thereby make them representable in PIR types)
• Language.PureScript.Environment defines the record type which serves as the typechecking context (it's often just called Context in other lambda calculus implementations). This holds mappings from names to types, as well as mappings from type synonyms to their expansions and mappings from type class names to type class dictionaries and TypeClassData
• The modules in the Language.PureScript.Sugar.TypeClasses namespace are relevant to us because we start working on the AST after typeclasses have been translated into explicit dictionaries and constrainted functions have been expanded into functions that take a Dict arg. This is kind of annoying! They never adjust the type of the functions. For example, if we have f :: Eq a => a -> a -> Bool, the underlying expression really has a type like f :: EqDict a -> a -> a -> Bool (but it's not clear to me whether this is uniform - like if the typeclass has no methods, does it still generate a dict and add it as an implicit arg? hard to tell!)
• The Language.PureScript.CoreFn namespace is where we're doing most of our work. You can compare their Language.PureScript.CoreFn.Expr types to the ones in my sean/typedCoreFn branch to get a sense of what we're trying to do. The bulk of the work we have to do in the PS compiler consists in rewriting Language.PureScript.CoreFn.Desugar to emit our typed CoreFn. (I am just replacing their untyped version with our typed version)
• Oh and it's probably good to be familiar with Language.PureScript.Names to get a sense of how to work w/ their identifiers.

Slack Message

[klntsky]

Some other minor notes:
• We want to leave all quantifiers where they are. This requires some finessing, as calls to their type inference machinery will try to instantiate the quantifiers to TUnknown types which have more restrictive unification conditions than regular TyVars.
• We're leaving in row types, but we will eliminate them during the final compilation pass where we an instantiate all polymorphic rows.
• Probably the single most frustrating thing about working on this is that we often have to look at the show representation of these AST types, which is very hard to read but contains information that cannot be conveniently pretty-printed. (The SourceSpan stuff matters because locally bound variables must be qualified by the source position at which they come into scope)
• In Language.PureScript.CoreFn.Desugar (in my working branch), the primary function is exprToCoreFn :: forall m. M m => ModuleName -> SourceSpan -> Maybe SourceType -> A.Expr -> m (Expr Ann) . (M is just a constraint synonym for a monad that has all of the typechecking capabilities we need). I'm mentioning this because we should prefer, wherever possible, to avoid inferring types that we can deduce. We do that by passing in a Just (t :: SourceType) to that function. For example, we should not ever need to infer the type of a lambda abstraction.

Slack Message