Copyright	(c) Julian Grove and Aaron Steven White 2025
License	MIT
Maintainer	julian.grove@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

Framework.Lambda.Types

Description

Types and type inference are defined. Types feature variables, quantified at the top level for some limited polymorphism. Constants may also be polymorphic.

Synopsis

arity :: Type -> Int
asTyped :: Sig -> (Term -> Term) -> Typed -> Typed
order :: Type -> Int
type Sig = Constant -> Maybe Type
ty :: Sig -> Term -> Typed
tyEq :: TypeRed -> TypeRel
tyEq' :: TypeRel
data Type
- = Atom String
- | Type :→ Type
- | Unit
- | Type :× Type
- | P Type
- | TyCon String [Type]
- | TyVar String
data Typed = Typed {
- termOf :: Term
- typeOf :: Maybe Type
}
unify :: Constr -> Maybe Constr

Documentation

arity :: Type -> Int Source #

asTyped :: Sig -> (Term -> Term) -> Typed -> Typed Source #

order :: Type -> Int Source #

type Sig = Constant -> Maybe Type Source #

Assign types to constants.

ty :: Sig -> Term -> Typed Source #

Provide a term along with its principal type, given a signature.

tyEq :: TypeRed -> TypeRel Source #

Determine if two types are semantically equivalent, taking type reductions into account.

tyEq' :: TypeRel Source #

Semantic type equality, taking popable types into account.

data Type Source #

Arrows, products, and probabilistic types, as well as (a) abstract type constructors, and (b) type variables for encoding polymorphism.

Constructors

Atom String
Type :→ Type infixr 5
Unit
Type :× Type infixl 6
P Type
TyCon String [Type]
TyVar String

Instances

Instances details

Show Type Source #
Instance details Defined in Framework.Lambda.Types Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
Eq Type Source #
Instance details Defined in Framework.Lambda.Types Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #

data Typed Source #

Typed terms (where not every term has a type).

Constructors

Typed
Fields termOf :: Term typeOf :: Maybe Type

Instances

Instances details

Show Typed Source #
Instance details Defined in Framework.Lambda.Types Methods showsPrec :: Int -> Typed -> ShowS # show :: Typed -> String # showList :: [Typed] -> ShowS #
Eq Typed Source #
Instance details Defined in Framework.Lambda.Types Methods (==) :: Typed -> Typed -> Bool # (/=) :: Typed -> Typed -> Bool #

unify :: Constr -> Maybe Constr Source #

Arrive at a most general unifier, or fail if none exists.