syntax-tree-0.1.0.0: Typed ASTs

Safe HaskellNone
LanguageHaskell2010

AST.Infer.Blame

Description

Hindley-Milner type inference with ergonomic blame assignment.

blame is a type-error blame assignment algorithm for languages with Hindley-Milner type inference, but without generalization of intermediate terms. This means that it is not suitable for languages with let-generalization. Let is an example of a term that is not suitable for this algorithm.

With the contemporary knowledge that "Let Should Not Be Generalised", as argued by luminaries such as Simon Peyton Jones, optimistically this limitation shouldn't apply to new programming languages. This blame assignment algorithm can also be used in a limited sense for existing languages, which do have let-generalization, to provide better type errors in specific definitions which don't happen to use generalizing terms.

The algorithm is pretty simple:

  • Invoke all the inferBody calls as infer normally would, but with one important difference: where inferBody would normally get the actual inference results of its child nodes, placeholders are generated in their place
  • Globally sort all of the tree nodes according to a given node prioritization (this prioritization would be custom for each language)
  • According to the order of prioritization, attempt to unify each infer-result with its placeholder using inferOfUnify. If a unification fails, roll back its state changes. The nodes whose unification failed are the ones assigned with type errors.

Lamdu uses this algorithm for its "insist type" feature, which moves around the blame for type mismatches.

Note: If a similar algorithm already existed somewhere, I would very much like to know!

Synopsis

Documentation

blame :: forall priority err m exp a. (Ord priority, MonadError err m, Blame m exp) => (a -> priority) -> Tree (InferOf exp) (UVarOf m) -> Tree (Ann a) exp -> m (Tree (BTerm a (UVarOf m)) exp) Source #

Perform Hindley-Milner type inference with prioritised blame for type error, given a prioritisation for the different nodes.

The purpose of the prioritisation is to place the errors in nodes where the resulting errors will be easier to understand.

The expected MonadError behavior is that catching errors rolls back their state changes (i.e StateT s (Either e) is suitable but EitherT e (State s) is not)

Gets the top-level type for the term for support of recursive definitions, where the top-level type of the term may be in the scope of the inference monad.

class (Infer m t, RTraversable t, KTraversable (InferOf t), KPointed (InferOf t)) => Blame m t where Source #

Class implementing some primitives needed by the blame algorithm

The blamableRecursive method represents that Blame applies to all recursive child nodes. It replaces context for Blame to avoid UndecidableSuperClasses.

Minimal complete definition

inferOfUnify, inferOfMatches

Methods

inferOfUnify :: Proxy t -> Tree (InferOf t) (UVarOf m) -> Tree (InferOf t) (UVarOf m) -> m () Source #

Unify the types/values in infer results

inferOfMatches :: Proxy t -> Tree (InferOf t) (UVarOf m) -> Tree (InferOf t) (UVarOf m) -> m Bool Source #

Check whether two infer results are the same

blamableRecursive :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Blame m)) Source #

blamableRecursive :: KNodesConstraint t (Blame m) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Blame m)) Source #

Instances
Recursive (Blame m) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

recurse :: (KNodes k, Blame m k) => Proxy (Blame m k) -> Dict (KNodesConstraint k (Blame m)) Source #

data BTerm a v e Source #

A Knot for an inferred term with type mismatches - the output of blame

Constructors

BTerm 

Fields

Instances
KNodes (Flip (BTerm a) e) Source # 
Instance details

Defined in AST.Infer.Blame

Associated Types

type KNodesConstraint (Flip (BTerm a) e) c :: Constraint Source #

data KWitness (Flip (BTerm a) e) a :: Type Source #

Methods

kLiftConstraint :: KNodesConstraint (Flip (BTerm a) e) c => KWitness (Flip (BTerm a) e) n -> Proxy c -> (c n -> r) -> r Source #

(Recursively KFunctor e, Recursively KFunctorInferOf e) => KFunctor (Flip (BTerm a) e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

mapK :: (forall (n :: Knot -> Type). KWitness (Flip (BTerm a) e) n -> Tree p n -> Tree q n) -> Tree (Flip (BTerm a) e) p -> Tree (Flip (BTerm a) e) q Source #

(Recursively KFoldable e, Recursively KFoldableInferOf e) => KFoldable (Flip (BTerm a) e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

foldMapK :: Monoid a0 => (forall (n :: Knot -> Type). KWitness (Flip (BTerm a) e) n -> Tree p n -> a0) -> Tree (Flip (BTerm a) e) p -> a0 Source #

(RTraversable e, RTraversableInferOf e) => KTraversable (Flip (BTerm a) e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

sequenceK :: Applicative f => Tree (Flip (BTerm a) e) (ContainedK f p) -> f (Tree (Flip (BTerm a) e) p) Source #

Constraints (BTerm a v e) Eq => Eq (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

(==) :: BTerm a v e -> BTerm a v e -> Bool #

(/=) :: BTerm a v e -> BTerm a v e -> Bool #

Constraints (BTerm a v e) Ord => Ord (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

compare :: BTerm a v e -> BTerm a v e -> Ordering #

(<) :: BTerm a v e -> BTerm a v e -> Bool #

(<=) :: BTerm a v e -> BTerm a v e -> Bool #

(>) :: BTerm a v e -> BTerm a v e -> Bool #

(>=) :: BTerm a v e -> BTerm a v e -> Bool #

max :: BTerm a v e -> BTerm a v e -> BTerm a v e #

min :: BTerm a v e -> BTerm a v e -> BTerm a v e #

Constraints (BTerm a v e) Show => Show (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

showsPrec :: Int -> BTerm a v e -> ShowS #

show :: BTerm a v e -> String #

showList :: [BTerm a v e] -> ShowS #

Generic (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Associated Types

type Rep (BTerm a v e) :: Type -> Type #

Methods

from :: BTerm a v e -> Rep (BTerm a v e) x #

to :: Rep (BTerm a v e) x -> BTerm a v e #

Constraints (BTerm a v e) Binary => Binary (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

put :: BTerm a v e -> Put #

get :: Get (BTerm a v e) #

putList :: [BTerm a v e] -> Put #

Constraints (BTerm a v e) NFData => NFData (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

Methods

rnf :: BTerm a v e -> () #

data KWitness (Flip (BTerm a) e) n Source # 
Instance details

Defined in AST.Infer.Blame

data KWitness (Flip (BTerm a) e) n where
type KNodesConstraint (Flip (BTerm a) e) c Source # 
Instance details

Defined in AST.Infer.Blame

type Rep (BTerm a v e) Source # 
Instance details

Defined in AST.Infer.Blame

type Rep (BTerm a v e) = D1 (MetaData "BTerm" "AST.Infer.Blame" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" False) (C1 (MetaCons "BTerm" PrefixI True) (S1 (MetaSel (Just "_bAnn") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Just "_bRes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either (InferOf' e v, InferOf' e v) (InferOf' e v))) :*: S1 (MetaSel (Just "_bVal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (e # BTerm a v)))))

type InferOf' e v = Tree (InferOf (GetKnot e)) v Source #

A type synonym to help BTerm be more succinct

bAnn :: forall a v e. Lens' (BTerm a v e) a Source #

bRes :: forall a v e. Lens' (BTerm a v e) (Either (InferOf' e v, InferOf' e v) (InferOf' e v)) Source #

bVal :: forall a v e. Lens' (BTerm a v e) ((#) e (BTerm a v)) Source #

bTermToAnn :: forall a v e r. Recursively KFunctor e => (forall n. KRecWitness e n -> a -> Either (Tree (InferOf n) v, Tree (InferOf n) v) (Tree (InferOf n) v) -> r) -> Tree (BTerm a v) e -> Tree (Ann r) e Source #