| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Types
Description
This is still a work in progress.
No really, what's this type system?
Eventually? I want
- Linear
- call-by-push-value with
- arbitrary rank type and kind polymorphism and
- graded (co)effects.
Papers and posts I am cribbing from:
Synopsis
- type TypeVar = Int
- data Type
- type Sigma = Type
- type Rho = Type
- type Tau = Type
- tyInt :: Rho
- tyFloat :: Rho
- tyBool :: Rho
- tyBottom :: Rho
- tyFunSig :: [Type] -> Type -> Type
- newtype Frame = Frame {}
- frameEmpty :: Frame
- frameExtend :: Frame -> (Symbol, Type) -> Frame
- frameRemove :: Frame -> Symbol -> Frame
- frameExtends :: Frame -> [(Symbol, Type)] -> Frame
- frameLookup :: Symbol -> Frame -> Maybe Type
- frameMerge :: Frame -> Frame -> Frame
- framesMerge :: [Frame] -> Frame
- frameSingleton :: Symbol -> Type -> Frame
- frameKeys :: Frame -> [Symbol]
- framesFromList :: [(Symbol, Type)] -> Frame
- framesToList :: Frame -> [(Symbol, Type)]
- type Infer = ReaderT Frame (StateT InferState (Except String))
- newtype InferState = InferState {}
- defaultInferState :: InferState
- runInfer :: Frame -> Infer a -> Either String a
- newtype Subst = Subst (Map TypeVar Rho)
- type Constraint = (Type, Type)
- type Unifier = (Subst, [Constraint])
- type Solve = Except String
- class Substitutable t where
- substitute :: Subst -> t -> t
- ftv :: t -> Set TypeVar
- typecheck :: Frame -> CbpvExp -> Either String Type
- closeOver :: Type -> Sigma
- normalize :: Sigma -> Sigma
- inFrame :: (Symbol, Type) -> Infer a -> Infer a
- inFrames :: [(Symbol, Type)] -> Infer a -> Infer a
- lookupInFrame :: Symbol -> Infer (Rho, [Constraint])
- fresh :: Infer Tau
- instantiate :: Sigma -> Infer Rho
- generalize :: Frame -> Rho -> Sigma
- getFrame :: Infer Frame
- skolemize :: Sigma -> Infer ([TypeVar], Rho)
- infer :: CbpvExp -> Infer (Rho, [Constraint])
- substEmpty :: Subst
- compose :: Subst -> Subst -> Subst
- runSolve :: [Constraint] -> Either String Subst
- solver :: Unifier -> Solve Subst
- unifies :: Type -> Type -> Solve Subst
- unifyMany :: [Type] -> [Type] -> Solve Subst
- bind :: TypeVar -> Type -> Solve Subst
- occursCheck :: Substitutable a => TypeVar -> a -> Bool
- solveInference :: [Constraint] -> (Subst -> Infer a) -> Infer a
- primType :: Symbol -> Maybe Sigma
- data Graph node key = Graph {}
- graphFromList :: Ord key => [(node, key, [key])] -> Graph node key
- vertexLabels :: Functor f => Graph b t -> f Vertex -> f b
- vertexLabel :: Graph b t -> Vertex -> b
- topo :: Graph node key -> [node]
- makeDepGraph :: Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol
(basic) Type language
Instances
| Show Type Source # | |
| Eq Type Source # | |
| Ord Type Source # | |
| Substitutable Constraint Source # | |
Defined in Types Methods substitute :: Subst -> Constraint -> Constraint Source # | |
| Substitutable Type Source # | |
Typing environment ("frame")
frameEmpty :: Frame Source #
framesMerge :: [Frame] -> Frame Source #
Inference monad
newtype InferState Source #
Constructors
| InferState | |
Constraint solving monad
type Constraint = (Type, Type) Source #
type Unifier = (Subst, [Constraint]) Source #
class Substitutable t where Source #
Instances
| Substitutable Constraint Source # | |
Defined in Types Methods substitute :: Subst -> Constraint -> Constraint Source # | |
| Substitutable Frame Source # | |
| Substitutable Type Source # | |
| Substitutable a => Substitutable [a] Source # | |
Inference
lookupInFrame :: Symbol -> Infer (Rho, [Constraint]) Source #
skolemize :: Sigma -> Infer ([TypeVar], Rho) Source #
Deep skolemization. Returns the skolem variables and the skolemized ρ-type.
infer :: CbpvExp -> Infer (Rho, [Constraint]) Source #
Type inference rules for CbpvExpressions.
All functions have at least one (terminal) argument of type ⊥.
Constraint solver
substEmpty :: Subst Source #
occursCheck :: Substitutable a => TypeVar -> a -> Bool Source #
solveInference :: [Constraint] -> (Subst -> Infer a) -> Infer a Source #
Graph implementation
graphFromList :: Ord key => [(node, key, [key])] -> Graph node key Source #
vertexLabel :: Graph b t -> Vertex -> b Source #