Skip to content

Instantly share code, notes, and snippets.

@jmikkola

jmikkola/typing_haskell_in_haskell.md

Last active August 29, 2015 14:25
Show Gist options
  • Save jmikkola/5c075a37cf91e1b17175 to your computer and use it in GitHub Desktop.
Save jmikkola/5c075a37cf91e1b17175 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
typing_haskell_in_haskell.md

Notes on Typing Haskell in Haskell

Conventions

Variable names:

  • kind: k (Kind)
  • type constructor: tc (Tycon)
  • type variable: v (Tyvar)
    • fixed type variable: f
    • generic type variable: g
  • type: t (Type)
  • class: c (Class)
  • instance: it (Instance)
  • predicate: p, q (Pred)
    • deferred predicate: d
    • retained predicate: r
  • qualified type: qt (QualType)
  • class environment: ce (ClassEnv)
  • scheme: sc (Scheme)
  • substitution: s (Subst)
  • unifier: u (Subst)
  • assumption: s (Assump)
  • identifier: i (Id)
  • literal: l (Literal)
  • pattern: pat (Pat)
  • expression: e, f, ... (Expr)
  • alternative: alt (Alt)
  • binding group: bg (BindGroup)

Glossary

  • identifier: a variable (or function) name
  • type: the possible forms a value can take (don't sue me, I know that's a bad definition)
  • kind: a description of how types need to be composed with other types (e.g. the kind of Int is *, the kind of (a, b) is * -> * -> *)
  • substitutions: a mapping of type variables to types (possibly other type varaiables).
  • merge: make sure two substitutions agree, then concatenate them.
  • unifier: a substitution that, when applied to two types, makes those types equal.
  • most general unifier (mgu): a unifier u such that any other unifier s can be written as s' @@ u for some substitution s'.
  • matching types: "Given two types t1 and t2, the goal of matching is to find a substitution s such that apply s t1 = t2." It's sometimes called "one-way matching."
  • predicate: a constraint on a type, requiring that a type variable be a member of a type class.
    • E.g. in (Num a) => a -> Int, the predicate is (Num a)
  • qualified: a type class restricted in how it can be instantiated by a list of predicates.
  • context: The list of predicates in a qualified type.
  • head: The actual type in a qualified type.
  • class environment: the type classes that currently exist
  • default types: in some situations, like show (1 + read "1"), the type can be ambiguous (read coult return either an Int or a Float and both would work). The default types are a list of what order to try types in when multiple can match.
  • head-normal form: class arguments of the form v t1 ... tn where v is a type variable and t1..tn are zero or more types (i.e. it starts with a variable).
    • Haskell requires that class arguments be in head normal form.
  • entail: a predicate is entailed by other predicates if it always holds when the others hold (it's like implication).
  • simplifying predicates: reducing a list of predicates to its minimal form by:
    • Removing duplicates
    • Eliminating predicates that are known to hold (like Num Int)
    • Simplifying using superclass info (e.g. [Eq a, Ord a] to just Ord a)
  • type scheme (or just scheme): a type along with a set of bound type variables (a bound type variable is one that is defined within the scheme itself).
  • quantify a type: replace all occurances of certain type variables with generic variables?
  • assumption: a scheme that we assume applies to a variable.
  • instantiate a type: replace all generic variables with other variables?
  • alternative: "An Alt specifies the left and right hand sides of a function definition" - huh?
    • I think that this is actually a way to express a list of possible ways to match things (e.g. in a case statement of function definition).
  • generalization: calculating the most general types that are possible.
  • ambiguous type scheme: A type scheme ps => t where ps contains generic variables that do not appear in t. (A generic in the predicate that's not in the type -- would that happen with rank-N types?) Example: stringInc x = show (read x + 1) -- what type does x have? The type of stringInc would be (Read a, Num a) => String -> String.
  • default types: a special feature of Haskell where it tries to resolve ambiguous types by trying some default types until it finds one that fits.

Meaning of Functions

  • enumId
    • Int -> Id
    • Creates an identifier from a number
  • fn (infix)
    • Type -> Type -> Type
    • A helper function that creates the type (a -> b) from the types a and b
  • list
    • Type -> Type
    • A helper function that creates the type [a] from the type a
  • pair
    • Type -> Type -> Type
    • A helper function that creates the type (a, b) from the types a and b
  • kind
    • t -> Kind
    • The function defined by the class HasKind
    • Finds the kind of a type
  • nullSubst
    • Subst
    • Creates an empty substitution
  • +-> (infix)
    • Tyvar -> Type -> Subst
    • Creates a list of substitutions with one substitution in it, replacing left side to the right side.
  • apply
    • Subst -> t -> t
    • A function in the class Types
    • Replaces parts of the type with their substitutions
  • tv
    • t -> [Tyvar]
    • A function in the class Types
    • Walks a type to find the set of all the type variables in it
  • @@ (infix)
    • Subst -> Subst -> Subst
    • "Composes" substitutions
    • apply (s1 @@ s2) is equivalent to apply s1 . apply s2
    • code: s1 @@ s2 = [ (u, apply s1 t) | (u,t) <- s2 ] ++ s1
    • It works by resubstituting anything in s2 that is substituted in s1, then merging the result with s1.
  • merge
    • Monad m => Subst -> Subst -> m Subst
    • Similar to @@
    • Requires that substitutions in the two agree (where they substitute the same variable).
    • Doesn't replace anything in one with anything from the other.
  • mgu
    • Monad m => Type -> Type -> m Subst
    • Finds (if possible) the most general unifier of two types (i.e. unifies)
  • varBind
    • Monad m => Tyvar -> Type -> m Subst
    • A helper function used in unifying a type variable with another type
  • match
    • Monad m => Type -> Type -> m Subst
    • matches two types
    • similar to mgu, except that it uses merge instead of @@ to combine substitutions.
  • mguPred
    • Pred -> Pred -> Maybe Subst
    • Defined as lift mgu
  • matchPred
    • Pred -> Pred -> Maybe Subst
    • Defined as lift match
    • Matches the heads of both predicates, assuming they have the same context.
  • lift
    • Applys the function (either mgu or match) to the head of both predicates, assuming both predicates have the same context.
    • i.e. it unifies the types if the conditions match.
    • Probably unifying the types will mostly be merging two type variables.
  • classes
    • ClassEnv -> (Id -> Maybe Class)
    • Gets the class mapping function out of a ClassEnv
  • defaults
    • ClassEnv -> [Type]
    • Gets the list of default types
  • super
    • ClassEnv -> Id -> [Id]
    • Looks up the parent classes for a given class name
  • insts
    • ClassEnv -> Id -> [Inst]
    • Looks up the instaces of a given class name
  • defined
    • Maybe a -> Bool
    • A helper function (basically "isJust")
  • modify
    • ClassEnv -> Id -> Class -> ClassEnv
    • Updates/Sets the definition of a class in the class environment
  • initialEnv
    • :: ClassEnv
    • Creates an empty set of classes
  • <:> (infix)
    • EnvTransformer -> EnvTransformer -> EnvTransformer
    • Composes two environment transformer functions into one.
    • Since environment transformers return a Maybe type, this is just lifting the two into the maybe monad.
  • addClass
    • Id -> [Id] -> EnvTransformer
    • Adds a new class (name is first arg, parents are secoond arg) to the environment.
    • Requires that all parents be defined already, so calls to this must be topologically sorted beforehand.
  • addPreludeClasses (also, addCoreClasses and addNumClasses)
    • :: EnvTransformer
    • helper functions to add default classes to the environment
  • addInst
    • [Pred] -> Pred -> EnvTransformer
    • Adds an instance to a class (the predicate in the second argument contains the name of the class this instance is being added to, so it doesn't need to be a separate argument.)
    • The first list of predicates is what must hold in order for this instance to be implemented / this predicate to hold.
  • overlap
    • Pred -> Pred -> Bool
    • A helper function that tests if there is some predicate that is a substitution instance of the heads of both instance declarations.
    • That can happen with two identical instances (e.g. two copies of Eq Int) or two cases that can unify (e.g. Eq [a] and Eq [Int]).
  • exampleInsts
    • :: EnvTransformer
    • a helper function that creates a default class environment with default classes and default instances
  • bySuper
    • ClassEnv -> Pred -> [Pred]
    • Result may contain duplicates
    • Returns the list of predicates that also hold when the given predicate holds becuase those predicates are superclasses of the class in the predicate (and if a type is an instance of a class, it's always also an instance of all of the superclasses of that class).
  • byInst
    • ClassEnv -> Pred -> Maybe [Pred]
    • Determines subgoals for a given predicate.
    • Gives the predicates that must be true for that predicate to hold by looking at the predicates for the matching instance of the class.
  • entail
    • ClassEnv -> [Pred] -> Pred -> Bool
    • Tests if the predicate is entailed by the list of predicates.
    • (uses bySuper and byInst)
    • It returns true if.f. p (third arg) holds true when all the predicates ps (second arg) also hold true.
    • This can be for one of two reasons:
      • The predicate p is already in the list ps or it's super classes
      • All the subgoals of p (as found by byInst) are entailed by ps
  • inHnf
    • Pred -> Bool
    • Short for: "in head-normal form"
  • toHnf
    • Monad m => ClassEnv -> Pred -> m [Pred]
    • Returns the predicate unchanged (but in a list) if it's already in HNF
    • Otherwise, it tries to convert all the subgoals (found using byInst) to HNF.
  • toHnfs
    • Monad m => ClassEnv -> [Pred] -> m [Pred]
    • Converts a list of predicates to HNF (basically concat $ mapM toHnf)
  • simplify
    • ClassEnv -> [Pred] -> [Pred]
    • simplifies a list of predicates.
    • Removes predicates that are entailed by other predicates.
  • reduce
    • Monad m => ClassEnv -> [Pred] -> m [Pred]
    • Converts all predicates to HNF then simplifies
    • (Pretty much just a convenience function)
  • scEntail
    • ClassEnv -> [Pred] -> Pred -> Bool
    • an alternative (faster?) entail function that could be used in simplify
  • quantify
    • [Tyvar] -> Qual Type -> Scheme (remember, Qual Type means [Pred] :=> Type)
    • quantifies a qualified type
  • toScheme
    • Type -> Scheme
    • Helper function that converts a type to a scheme with no kinds and no predicates
  • find
    • Monad m => Id -> [Assump] -> m Scheme
    • Helper function that looks up a scheme by the variable associated with it
  • runTI
    • TI a -> a
    • helper function to run the TI monad
  • getSubst
    • TI Subst
    • returns the current substitution in the TI monad
    • e.g. s <- getSubst
  • unify
    • Type -> Type -> TI ()
    • Extends the substitution with the most general unifier of its arguments
  • extSubst
    • Subst -> TI ()
    • Helper function that extends the current substitution in the TI monad
    • Uses @@ to combine the new substitution with the current one.
  • newTVar
    • Kind -> TI Type
    • Creates a new type variable (with a unique name) of the given kind (in the TI monad).
  • freshInst
    • Scheme -> TI (Qual Type)
    • Creates new type variables for each kind in the scheme, then instantiates the qualified type with them.
  • inst
    • [Type] -> t -> t
    • Defined by the class Instantiate
    • A variation of apply that works on generic variables
    • It replaces each occurrence of a generic variable TGen n in t with ts !! n.
  • tiLit
    • Literal -> TI ([Pred], Type)
    • Gets the type for a literal value in the inference monad
    • Some literals (e.g. Char) get a complete type (e.g. ([], tChar))
    • Others (e.g. Int) get a type var + predicate (e.g. ([IsIn "Num" v], v))
  • tiPat
    • Pat -> TI ([Pred], [Assump], Type)
    • Gets the type of the thing that the pattern matches along with (in the assumptions) information about any variable that gets introduced.
  • tiPats
    • [Pat] -> Ti ([Pred], [Assump], Type)
    • A variant of tiPat that works on lists of patterns (to make life easier)
  • tiExpr
    • Infer Expr Type
      • == ClassEnv -> [Assump] -> Expr -> Ti ([Pred], Type)
    • does type inference for expressions
    • For variables and constants, the result is what you get from making a fresh instantiation of the scheme.
      • TODO: why? Are constants polymorphic?
    • Inferring the type of an application of expressions works by first inferring the type of the two expressions, then unifies the type of the left expression (which should be a function) with the type tf -> t where tf is the type of the right expression and t is a new type variable (apparently representing the return value).
    • To infer the type of a let binding, it uses tiBindingGroup (not defined yet!) and types the epxression using those assumptions (TODO: understand this better).
  • tiAlt
    • Infer Alt Type
      • == ClassEnv -> [Assump] -> Alt -> Ti ([Pred], Type)
    • Does type inference for an alternative
    • It types the patterns, then types the expressions using the assumptions from typing the patterns (TODO: understand the implications of using the assumptions), and finally returns a function type that takes as aguments the values in the pattern and returns the type of the expression.
  • tiAlts
    • ClassEnv -> [Assump] -> [Alt] -> Type -> Ti [Pred]
    • why does this take a type and not return a list of types?
      • Because it's checking that all the alternatives aggree with that type, it's not using them to figure out the type (?) / it's probably adding the type to the inference monad.
  • split
    • Monad m => ClassEnv -> [Tyvar] -> [Tyvar] -> [Pred] -> m ([Pred], [Pred])
    • Does three things:
      • Performs context reduction
      • Identifies deferred predicates
      • Eliminates some predicates using defaults
  • ambiguities
    • ClassEnv -> [Tyvar] -> [Pred] -> [Ambiguity]
    • Finds type ambiguities
    • It works by:
      • Finding type variables in the predicates that are not in the given list of type variables.
      • For each of those, finding the predicates that mention that type variable.
  • candidates
    • ClassEnv -> Ambiguity -> [Type]
    • Finds candidates for resolving a particular ambiguity
    • Uses the 4 rules for picking defaults to find the types (if any) that can be used as defaults for the ambiguity.
  • withDefaults
    • Monad m => ([Ambiguity] -> [Type] -> a) -> ClassEnv -> [Tyvar] -> [Pred] -> m a
    • Finds ambiguities and resolves them using the given function.
    • (Fails if any of the ambiguous types can't be defaulted)
  • defaultedPreds
    • Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred]
    • Uses withDefaults to get a list of all predicates for ambiguous types.
  • defaultSubst
    • Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m Subst
    • Uses withDefaults to build a substitution that applies the defaults.
    • It gets all the ambiguous types variables from the ambiguities and maps them to the default type for those variables.

Classes

  • HasKind
    • Instances: Tyvar, Tycoon, Type
    • Functions: kind
  • Types
    • Instances: Type, [Types], Qual Types, Scheme, Assumption
    • Functions: apply, tv
  • Monad (defined elsewhere)
    • Instances: TI
  • Instantiate
    • Instances: Type, Pred, [Instantiate], Qual [Instantiate]
    • Functions: inst

Types

  • Id
    • type Id = String
    • an identifier
    • Depending on the context, this can be a variable, a type variable, or the name of a type constructor.
  • Kind (Star or Kfun)
    • data Kind = Star | Kfun Kind Kind
    • Represents a kind
  • Type (TVar, TCon, TAp, or TGen)
    • data Type = TVar Tyvar | TCon Tycon | TAp Type Type | TGen Int
    • Represents a type
    • E.g. tArrow = TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))
      • Arrow means function
    • TVar is a type variable (like a)
    • TCon is a type constructor (like Either)
    • TGen stores a generic type variable, identified only by an integer.
  • TAp applies a type constructor to other types (e.g. TAp tList tInt)
  • Tyvar
    • data Tyvar = Tyvar Id Kind
    • Stores a type variable and the kind of type that variable must have.
  • Tycon
    • data Tycon = Tycon Id Kind
    • Represents a type constructor and what kind of type it is
    • e.g. tList = TCon (Tycon "[]" (Kfun Star Star))
  • Subst
    • type Subst = [(Tyvar, Type)]
    • A mapping from type variable to its current substitution
  • Pred (IsIn)
    • data Pred = IsIn Id Type
    • Stores a predicate on a type variable.
  • Qual (:=>)
    • data Qual t = [Pred] :=> t
    • Stores a type qualified by a list of 0+ predicates
  • Class
    • type Class = ([Id], [Inst])
    • Used to represent a class
    • The first list ([Id]) is the list of super classes (e.g. Eq is a superclass of Ord).
    • The second list ([Inst]) stores instances of that class (each of which is qualified, because Inst is an alias for a qualified predicate).
  • Inst
    • type Inst = Qual Pred
    • Used to represent an instance of a class.
    • Expands to [Pred] :=> Pred
    • It means that a predicate (on the right) is true if the list of predicates on the left hold.
  • ClassEnv
    • Fields:
      • classes :: ID -> Maybe Class
      • defaults :: [Type]
    • Represents a class environment
  • EnvTransformer
    • type EnvTransformer = ClassEnv -> Maybe ClassEnv
    • A type used for functions that modify class environments, with the possibility of an error.
  • Scheme (Forall)
    • data Scheme = Forall [Kind] (Qual Type)
    • "Type schemes are used to represent polymorphic types"
    • Represents a type scheme
    • Contains:
      • A list of Kinds (used as a mapping between integers and kinds). These are the kinds for any generic types that appear in the qualified type.
        • TGen n has kind ks !! n
      • A qualified type (a list of predicates and a type).
  • Assump (:>:)
    • data Assump = Id :>: Scheme
    • Represents an assumption
  • TI (i.e. Type Inference)
    • newtype TI a = TI (Subst -> Int -> (Subst, Int, a))
    • An instance of Monad
    • Maintains the current substitution and the next number to use when generating type variables.
  • Infer
    • type Infer e t = ClassEnv -> [Assump] -> e -> TI ([Pred], t)
    • Infer is a type alias for convenience.
    • Most typing rules are variants of it.
  • Literal (LitInt, LitChar, LitRat, LitStr)
    • data Literal = ...
    • Represents a literal value in the code to be typped
  • Pat (PVar, PWildcard, PAs, PLit, PNpk, PCon)
    • data Pat =
      • PVar Id
      • PWildcard
      • PAs Id Pat
      • PLit Literal
      • PNpk Id Integer
      • PCon Assump [Pat]
    • Represents a pattern (e.g. in a case statement)
  • Expr (Var, Lit, Const, Ap, Let)
    • data Expr =
      • Var Id
      • Lit Literal
      • Const Assump
      • Ap Expr Expr
      • Let BindingGroup
    • Represents an expression
  • Alt
    • type Alt = ([Pat], Expr)
    • Represents an alternative
  • Ambiguity
    • type Ambiguity = (Tyvar, [Pred])
    • Represents a type ambiguity
    • The first part is the type variable that is ambiguous
    • The second part is the predicates known for that type var

Exploring functions

byInst

byInst                   :: ClassEnv -> Pred -> Maybe [Pred]
byInst ce p@(IsIn i t)    = msum [ tryInst it | it <- insts ce i ]
 where tryInst (ps :=> h) = do u <- matchPred h p
                               Just (map (apply u) ps)

Relevant bits:

  • ClassEnv: classes (ID -> Maybe Class) and defaults ([Type])
  • Pred: IsIn Id Type
  • Qual: [Pred] :=> t
  • matchPred: Matches the heads of both predicates, assuming they have the same context.
  • apply: Replaces parts of the type with their substitutions.
    • Subst -> t -> t

it is one of the instance instances of class i, which is the class in the predicate.

tryInst matches the head (a Pred in this case) of the instance with the given predicate (i.e. sees if it could be made to match by making it more specific). If it succeeds, it then applies the substitution that resulted from matching to the context of the instance. The result of that is what gets returned.

Example:

Say the predicate is IsIn "Ord" "Eq [Int]" (I'm not sure if that totally makes sense). It might find a matching instance Eq [a] with the other predicate IsIn "Ord" "a". That instance would match with the substitution a +-> Int. When applied to the predicates, you get IsIn "Ord" "Int".

quantify

code:

quantify      :: [Tyvar] -> Qual Type -> Scheme
quantify vs qt = Forall ks (apply s qt)
 where vs' = [ v | v <- tv qt, v `elem` vs ]
       ks  = map kind vs'
       s   = zip vs' (map TGen [0..])

vs' is the list of the type variables in qt (2nd arg) that appear in vs (1st arg). ks is a list of the kinds of vs'. s is a list of tuples where the first element is one of vs' and the second is a TGen with a unique number.

The result is a type scheme with the kinds ks and the qualified type resulting from applying s to qt.

This is finding the type variables in the qualified type that also appear in the first arg, creating generic variables of the same kind, and then substituting those generic variables in for the type variables.

References:

  • Types
    • Tyvar (Tyvar Id Kind)
    • Qual Type (=== to [Pred] :=> Type)
    • Pred (IsIn Id Type)
    • Scheme (Forall [Kind] (Qual Type))
    • Type (TGen Int)
  • Functions
    • apply (Subst -> t -> t, of class Types): Replaces things with thir substitutions.
    • kind (t -> Kind, of class HasKind): Finds the kind of a type
    • tv (t -> [Tyvar], of class Types): Finds all type variables.

tiPat (for constructors)

tiPat (PCon (i:>:sc) pats) = do
    (ps,as,ts) <- tiPats pats
    t'         <- newTVar Star
    (qs :=> t) <- freshInst sc
    unify t (foldr fn t' ts)
    return (ps++qs, as, t')

By lines:

  • Type inference for all the sub patterns
  • Create a new type variable with kind *
  • Instantiates the given scheme (replacing generic variables)
  • Unifies the type resulting from instantiating the scheme with the type of a function that takes the parameters to the constructor and returns the new type variable.a c
  • Adds the predicates from instantiating the scheme to the list of predicates and returns the new type variable.

References:

  • Types
    • Pat
    • Assump (data Assump = Id :>: Scheme)
    • Scheme (Forall [Kind] (Qual Type))
    • Qual (data Qual t = [Pred] :=> t)
  • Functioons
    • tiPats ([Pat] -> Ti ([Pred], [Assump], Type))
    • newTVar (Kind -> TI Type)
    • freshInst (Scheme -> TI (Qual Type))
    • fn (Type -> Type -> Type)

split

Code:

split :: Monad m => ClassEnv -> [Tyvar] -> [Tyvar] -> [Pred]
                    -> m ([Pred], [Pred])
split ce fs gs ps = do
    ps' <- reduce ce ps
    let (ds, rs) = partition (all (`elem` fs) . tv) ps'
    rs' <- defaultedPreds ce (fs++gs) rs
    return (ds, rs \\ rs')

Some things which this function may or may not do:

  • Simplify the list of predicates (it looks like this does happen, using reduce)
  • Defer "fixed" variables (those that appear in assumptions) to the enclosing bindings (huh?)
  • Use default types in when there is ambiguity. It seems to do this with defaultedPreds.

It breaks the list of predicates into deferred predicates (ds) and retained predicates (rs). The retained predicates are the ones that become part of the type (rs :=> t) while the deferred predicates become constraints for the enclosing scope. The deferred predicates are the ones "that contain only fixed type variables." (TODO: what does it mean for a type variable to be "fixed"?)

It determines which of the two groups to put a predicate in by the output of a inner function. That function first takes all the type variables in the predicate (using tv), then tests if they are all elements of the given list of type variables fs. If they all are, the predicate goes in the list of deferred predicates.

It returns a tuple containing the list of deferred predicates and a list of the retained predicates that are not in the list of defaulted predicates (i.e. it removes the predicates that are replaced with a default type)

Aguments:

  • ce (ClassEnv)
  • fs ([Tyvar]) "Fixed" variables -- "the variables appearing free in the assumptions" (TODO: what does that mean?)
  • gs ([Tyvar]) The set of variables over which we would like to quantify.
  • ps ([Pred])

References:

  • Types
    • ClassEnv (classes Id -> Maybe Class, defaults [Type])
    • Class type Class = ([Id], [Inst])
    • Tyvar Tyvar Id Kind
    • Pred IsIn Id Type
  • Functions
    • reduce Monad m => ClassEnv -> [Pred] -> m [Pred] Converts all predicates to HNF then simplifies.
    • partition (from Data.List), (a -> Bool) -> [a] -> ([a], [a])
    • defaultedPreds Monad m => ClassEnv -> [Tyvar] -> [Pred] -> m [Pred]
    • \\ (infix, from Data.List) Eq a => [a] -> [a] -> [a] List difference.
    • elem (from prelude) Eq a -> a -> t a -> Bool Tests for inclusion.

Notes

Defaulting

Rules for when defaulting is allowed:

  • All of the predicates are in the form IsIn c (TVar v) where c is a class.
  • At least one of the classes is a standard numeric class (one of: Num, Integral, Floating, Fractional, Real, RealFloat, RealFrac)
  • All of the classes involved are standard elasses (which includes the numeric classes, plus things like Eq, Ord, Show, Functor, etc)
  • There is at least one type in the list of default types that is an instance of all the mentioned classes.

The first type in the list of defaults that matches is the one that gets used.

Open questions

  • Near the end of section 4, it talks about being able to figure out the kind of TAp t t' using only t, assuming it's well-formed. If it's well-formed, wouldn't the kind always end up being just * in the end?
  • What really is an alternative?
  • How does a type scheme (/ an assumption) capture that some variables must be a type compatible with the type of some function (for let polymorphism), even when that type isn't known yet?
    • Does the type scheme include the type variable of the thing that it must be a subtype of?
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment