disco-0.1.5: Functional programming language for teaching discrete math.
Copyrightdisco team and contributors
Maintainerbyorgey@gmail.com
Safe HaskellNone
LanguageHaskell2010

Disco.Types

Description

The Disco.Types module defines the set of types used in the disco language type system, along with various utility functions.

Synopsis

Disco language types

Atomic types

data BaseTy where Source #

Base types are the built-in types which form the basis of the disco type system, out of which more complex types can be built.

Constructors

Void :: BaseTy

The void type, with no inhabitants.

Unit :: BaseTy

The unit type, with one inhabitant.

B :: BaseTy

Booleans.

P :: BaseTy

Propositions.

N :: BaseTy

Natural numbers.

Z :: BaseTy

Integers.

F :: BaseTy

Fractionals (i.e. nonnegative rationals).

Q :: BaseTy

Rationals.

C :: BaseTy

Unicode characters.

CtrSet :: BaseTy

Set container type. It's a bit odd putting these here since they have kind * -> * and all the other base types have kind *; but there's nothing fundamentally wrong with it and in particular this allows us to reuse all the existing constraint solving machinery for container subtyping.

CtrBag :: BaseTy

Bag container type.

CtrList :: BaseTy

List container type.

Instances

Instances details
Eq BaseTy Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: BaseTy -> BaseTy -> Bool #

(/=) :: BaseTy -> BaseTy -> Bool #

Data BaseTy Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BaseTy -> c BaseTy #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BaseTy #

toConstr :: BaseTy -> Constr #

dataTypeOf :: BaseTy -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BaseTy) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseTy) #

gmapT :: (forall b. Data b => b -> b) -> BaseTy -> BaseTy #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseTy -> r #

gmapQ :: (forall d. Data d => d -> u) -> BaseTy -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BaseTy -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseTy -> m BaseTy #

Ord BaseTy Source # 
Instance details

Defined in Disco.Types

Show BaseTy Source # 
Instance details

Defined in Disco.Types

Generic BaseTy Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep BaseTy :: Type -> Type #

Methods

from :: BaseTy -> Rep BaseTy x #

to :: Rep BaseTy x -> BaseTy #

Alpha BaseTy Source # 
Instance details

Defined in Disco.Types

Pretty BaseTy Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => BaseTy -> Sem r Doc Source #

Subst Type BaseTy Source # 
Instance details

Defined in Disco.Types

Subst UAtom BaseTy Source # 
Instance details

Defined in Disco.Types

Subst Atom BaseTy Source # 
Instance details

Defined in Disco.Types

Subst BaseTy UAtom Source # 
Instance details

Defined in Disco.Types

Subst BaseTy BaseTy Source # 
Instance details

Defined in Disco.Types

type Rep BaseTy Source # 
Instance details

Defined in Disco.Types

type Rep BaseTy = D1 ('MetaData "BaseTy" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (((C1 ('MetaCons "Void" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Unit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "B" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "P" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "N" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Z" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "F" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Q" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "C" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "CtrSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CtrBag" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CtrList" 'PrefixI 'False) (U1 :: Type -> Type)))))

isCtr :: BaseTy -> Bool Source #

Test whether a BaseTy is a container (set, bag, or list).

data Var where Source #

Var represents type variables, that is, variables which stand for some type.

Constructors

V :: Ilk -> Name Type -> Var 

Instances

Instances details
Eq Var Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Data Var Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var -> c Var #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var #

toConstr :: Var -> Constr #

dataTypeOf :: Var -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Var) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var) #

gmapT :: (forall b. Data b => b -> b) -> Var -> Var #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r #

gmapQ :: (forall d. Data d => d -> u) -> Var -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var -> m Var #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var #

Ord Var Source # 
Instance details

Defined in Disco.Types

Methods

compare :: Var -> Var -> Ordering #

(<) :: Var -> Var -> Bool #

(<=) :: Var -> Var -> Bool #

(>) :: Var -> Var -> Bool #

(>=) :: Var -> Var -> Bool #

max :: Var -> Var -> Var #

min :: Var -> Var -> Var #

Show Var Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> Var -> ShowS #

show :: Var -> String #

showList :: [Var] -> ShowS #

Generic Var Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Var :: Type -> Type #

Methods

from :: Var -> Rep Var x #

to :: Rep Var x -> Var #

Alpha Var Source # 
Instance details

Defined in Disco.Types

Subst Type Var Source # 
Instance details

Defined in Disco.Types

Subst Atom Var Source # 
Instance details

Defined in Disco.Types

type Rep Var Source # 
Instance details

Defined in Disco.Types

data Ilk Source #

Var represents type variables, that is, variables which stand for some type. There are two kinds of type variables:

  • Unification variables stand for an unknown type, about which we might learn additional information during the typechecking process. For example, given a function of type List a -> List a, if we typecheck an application of the function to the list [1,2,3], we would learn that List a has to be List N, and hence that a has to be N.
  • Skolem variables stand for a fixed generic type, and are used to typecheck universally quantified type signatures (i.e. type signatures which contain type variables). For example, if a function has the declared type List a -> N, it amounts to a claim that the function will work no matter what type is substituted for a. We check this by making up a new skolem variable for a. Skolem variables are equal to themselves, but nothing else. In contrast to a unification variable, "learning something" about a skolem variable is an error: it means that the function will only work for certain types, in contradiction to its claim to work for any type at all.

Constructors

Skolem 
Unification 

Instances

Instances details
Eq Ilk Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: Ilk -> Ilk -> Bool #

(/=) :: Ilk -> Ilk -> Bool #

Data Ilk Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ilk -> c Ilk #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ilk #

toConstr :: Ilk -> Constr #

dataTypeOf :: Ilk -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Ilk) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ilk) #

gmapT :: (forall b. Data b => b -> b) -> Ilk -> Ilk #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ilk -> r #

gmapQ :: (forall d. Data d => d -> u) -> Ilk -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ilk -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ilk -> m Ilk #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ilk -> m Ilk #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ilk -> m Ilk #

Ord Ilk Source # 
Instance details

Defined in Disco.Types

Methods

compare :: Ilk -> Ilk -> Ordering #

(<) :: Ilk -> Ilk -> Bool #

(<=) :: Ilk -> Ilk -> Bool #

(>) :: Ilk -> Ilk -> Bool #

(>=) :: Ilk -> Ilk -> Bool #

max :: Ilk -> Ilk -> Ilk #

min :: Ilk -> Ilk -> Ilk #

Read Ilk Source # 
Instance details

Defined in Disco.Types

Show Ilk Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> Ilk -> ShowS #

show :: Ilk -> String #

showList :: [Ilk] -> ShowS #

Generic Ilk Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Ilk :: Type -> Type #

Methods

from :: Ilk -> Rep Ilk x #

to :: Rep Ilk x -> Ilk #

Alpha Ilk Source # 
Instance details

Defined in Disco.Types

Pretty Ilk Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Ilk -> Sem r Doc Source #

Subst Type Ilk Source # 
Instance details

Defined in Disco.Types

Subst Atom Ilk Source # 
Instance details

Defined in Disco.Types

type Rep Ilk Source # 
Instance details

Defined in Disco.Types

type Rep Ilk = D1 ('MetaData "Ilk" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Skolem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unification" 'PrefixI 'False) (U1 :: Type -> Type))

pattern U :: Name Type -> Var Source #

pattern S :: Name Type -> Var Source #

data Atom where Source #

An atomic type is either a base type or a type variable. The alternative is a compound type which is built out of type constructors. The reason we split out the concept of atomic types into its own data type Atom is because constraints involving compound types can always be simplified/translated into constraints involving only atomic types. After that simplification step, we want to be able to work with collections of constraints that are guaranteed to contain only atomic types.

Constructors

AVar :: Var -> Atom 
ABase :: BaseTy -> Atom 

Instances

Instances details
Eq Atom Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: Atom -> Atom -> Bool #

(/=) :: Atom -> Atom -> Bool #

Data Atom Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Atom -> c Atom #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Atom #

toConstr :: Atom -> Constr #

dataTypeOf :: Atom -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Atom) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Atom) #

gmapT :: (forall b. Data b => b -> b) -> Atom -> Atom #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Atom -> r #

gmapQ :: (forall d. Data d => d -> u) -> Atom -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Atom -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Atom -> m Atom #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Atom -> m Atom #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Atom -> m Atom #

Ord Atom Source # 
Instance details

Defined in Disco.Types

Methods

compare :: Atom -> Atom -> Ordering #

(<) :: Atom -> Atom -> Bool #

(<=) :: Atom -> Atom -> Bool #

(>) :: Atom -> Atom -> Bool #

(>=) :: Atom -> Atom -> Bool #

max :: Atom -> Atom -> Atom #

min :: Atom -> Atom -> Atom #

Show Atom Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> Atom -> ShowS #

show :: Atom -> String #

showList :: [Atom] -> ShowS #

Generic Atom Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Atom :: Type -> Type #

Methods

from :: Atom -> Rep Atom x #

to :: Rep Atom x -> Atom #

Alpha Atom Source # 
Instance details

Defined in Disco.Types

Pretty Atom Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Atom -> Sem r Doc Source #

Subst Type Atom Source # 
Instance details

Defined in Disco.Types

Subst Atom Atom Source # 
Instance details

Defined in Disco.Types

Subst Atom Var Source # 
Instance details

Defined in Disco.Types

Subst Atom Ilk Source # 
Instance details

Defined in Disco.Types

Subst Atom BaseTy Source # 
Instance details

Defined in Disco.Types

type Rep Atom Source # 
Instance details

Defined in Disco.Types

type Rep Atom = D1 ('MetaData "Atom" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "AVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Var)) :+: C1 ('MetaCons "ABase" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BaseTy)))

isVar :: Atom -> Bool Source #

Is this atomic type a variable?

isBase :: Atom -> Bool Source #

Is this atomic type a base type?

isSkolem :: Atom -> Bool Source #

Is this atomic type a skolem variable?

data UAtom where Source #

Unifiable atomic types are the same as atomic types but without skolem variables. Hence, a unifiable atomic type is either a base type or a unification variable.

Again, the reason this has its own type is that at some stage of the typechecking/constraint solving process, these should be the only things around; we can get rid of skolem variables because either they impose no constraints, or result in an error if they are related to something other than themselves. After checking these things, we can just focus on base types and unification variables.

Constructors

UB :: BaseTy -> UAtom 
UV :: Name Type -> UAtom 

Instances

Instances details
Eq UAtom Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: UAtom -> UAtom -> Bool #

(/=) :: UAtom -> UAtom -> Bool #

Ord UAtom Source # 
Instance details

Defined in Disco.Types

Methods

compare :: UAtom -> UAtom -> Ordering #

(<) :: UAtom -> UAtom -> Bool #

(<=) :: UAtom -> UAtom -> Bool #

(>) :: UAtom -> UAtom -> Bool #

(>=) :: UAtom -> UAtom -> Bool #

max :: UAtom -> UAtom -> UAtom #

min :: UAtom -> UAtom -> UAtom #

Show UAtom Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> UAtom -> ShowS #

show :: UAtom -> String #

showList :: [UAtom] -> ShowS #

Generic UAtom Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep UAtom :: Type -> Type #

Methods

from :: UAtom -> Rep UAtom x #

to :: Rep UAtom x -> UAtom #

Alpha UAtom Source # 
Instance details

Defined in Disco.Types

Pretty UAtom Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => UAtom -> Sem r Doc Source #

Subst UAtom UAtom Source # 
Instance details

Defined in Disco.Types

Subst UAtom BaseTy Source # 
Instance details

Defined in Disco.Types

Subst BaseTy UAtom Source # 
Instance details

Defined in Disco.Types

type Rep UAtom Source # 
Instance details

Defined in Disco.Types

uisVar :: UAtom -> Bool Source #

Is this unifiable atomic type a (unification) variable?

uatomToAtom :: UAtom -> Atom Source #

Convert a unifiable atomic type into a regular atomic type.

uatomToEither :: UAtom -> Either BaseTy (Name Type) Source #

Convert a unifiable atomic type to an explicit Either type.

Type constructors

data Con where Source #

Compound types, such as functions, product types, and sum types, are an application of a type constructor to one or more argument types.

Constructors

CArr :: Con

Function type constructor, T1 -> T2.

CProd :: Con

Product type constructor, T1 * T2.

CSum :: Con

Sum type constructor, T1 + T2.

CContainer :: Atom -> Con

Container type (list, bag, or set) constructor. Note this looks like it could contain any Atom, but it will only ever contain either a type variable or a CtrList, CtrBag, or CtrSet.

See also CList, CBag, and CSet.

CMap :: Con

Key value maps, Map k v

CGraph :: Con

Graph constructor, Graph a

CUser :: String -> Con

The name of a user defined algebraic datatype.

Instances

Instances details
Eq Con Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: Con -> Con -> Bool #

(/=) :: Con -> Con -> Bool #

Data Con Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Con -> c Con #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Con #

toConstr :: Con -> Constr #

dataTypeOf :: Con -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Con) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Con) #

gmapT :: (forall b. Data b => b -> b) -> Con -> Con #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Con -> r #

gmapQ :: (forall d. Data d => d -> u) -> Con -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Con -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Con -> m Con #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Con -> m Con #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Con -> m Con #

Ord Con Source # 
Instance details

Defined in Disco.Types

Methods

compare :: Con -> Con -> Ordering #

(<) :: Con -> Con -> Bool #

(<=) :: Con -> Con -> Bool #

(>) :: Con -> Con -> Bool #

(>=) :: Con -> Con -> Bool #

max :: Con -> Con -> Con #

min :: Con -> Con -> Con #

Show Con Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> Con -> ShowS #

show :: Con -> String #

showList :: [Con] -> ShowS #

Generic Con Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Con :: Type -> Type #

Methods

from :: Con -> Rep Con x #

to :: Rep Con x -> Con #

Alpha Con Source # 
Instance details

Defined in Disco.Types

Pretty Con Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Con -> Sem r Doc Source #

Subst Type Con Source # 
Instance details

Defined in Disco.Types

type Rep Con Source # 
Instance details

Defined in Disco.Types

type Rep Con = D1 ('MetaData "Con" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) ((C1 ('MetaCons "CArr" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CProd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CSum" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CContainer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Atom)) :+: C1 ('MetaCons "CMap" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CGraph" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))

pattern CList :: Con Source #

CList is provided for convenience; it represents a list type constructor (i.e. List a).

pattern CBag :: Con Source #

CBag is provided for convenience; it represents a bag type constructor (i.e. Bag a).

pattern CSet :: Con Source #

CSet is provided for convenience; it represents a set type constructor (i.e. Set a).

Types

data Type where Source #

The main data type for representing types in the disco language. A type can be either an atomic type, or the application of a type constructor to one or more type arguments.

Types are broken down into two cases (TyAtom and TyCon) for ease of implementation: there are many situations where all atoms can be handled generically in one way and all type constructors can be handled generically in another. However, using this representation to write down specific types is tedious; for example, to represent the type N -> a one must write something like TyCon CArr [TyAtom (ABase N), TyAtom (AVar (U a))]. For this reason, pattern synonyms such as :->:, TyN, and TyVar are provided so that one can use them to construct and pattern-match on types when convenient. For example, using these synonyms the foregoing example can be written TyN :->: TyVar a.

Constructors

TyAtom :: Atom -> Type

Atomic types (variables and base types), e.g. N, Bool, etc.

TyCon :: Con -> [Type] -> Type

Application of a type constructor to type arguments, e.g. N -> Bool is the application of the arrow type constructor to the arguments N and Bool.

Instances

Instances details
Eq Type Source # 
Instance details

Defined in Disco.Types

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Data Type Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type #

toConstr :: Type -> Constr #

dataTypeOf :: Type -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Type) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type) #

gmapT :: (forall b. Data b => b -> b) -> Type -> Type #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r #

gmapQ :: (forall d. Data d => d -> u) -> Type -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type #

Ord Type Source # 
Instance details

Defined in Disco.Types

Methods

compare :: Type -> Type -> Ordering #

(<) :: Type -> Type -> Bool #

(<=) :: Type -> Type -> Bool #

(>) :: Type -> Type -> Bool #

(>=) :: Type -> Type -> Bool #

max :: Type -> Type -> Type #

min :: Type -> Type -> Type #

Show Type Source # 
Instance details

Defined in Disco.Types

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Generic Type Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Type :: Type -> Type #

Methods

from :: Type -> Rep Type x #

to :: Rep Type x -> Type #

Alpha Type Source # 
Instance details

Defined in Disco.Types

Pretty Type Source # 
Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Type -> Sem r Doc Source #

Subst Type Rational Source # 
Instance details

Defined in Disco.Types

Subst Type Void Source # 
Instance details

Defined in Disco.Types

Subst Type Qualifier Source # 
Instance details

Defined in Disco.Types

Subst Type PolyType Source # 
Instance details

Defined in Disco.Types

Subst Type Type Source # 
Instance details

Defined in Disco.Types

Subst Type Con Source # 
Instance details

Defined in Disco.Types

Subst Type Atom Source # 
Instance details

Defined in Disco.Types

Subst Type Var Source # 
Instance details

Defined in Disco.Types

Subst Type Ilk Source # 
Instance details

Defined in Disco.Types

Subst Type BaseTy Source # 
Instance details

Defined in Disco.Types

Subst Type NameProvenance Source # 
Instance details

Defined in Disco.Names

Subst Type ModuleName Source # 
Instance details

Defined in Disco.Names

Subst Type ModuleProvenance Source # 
Instance details

Defined in Disco.Names

Subst Type Quantifier Source # 
Instance details

Defined in Disco.AST.Generic

Subst Type Constraint Source # 
Instance details

Defined in Disco.Typecheck.Constraints

Subst Type SimpleConstraint Source # 
Instance details

Defined in Disco.Typecheck.Solve

Subst Type Defn Source # 
Instance details

Defined in Disco.Module

Subst Type (QName a) Source # 
Instance details

Defined in Disco.Names

Methods

isvar :: QName a -> Maybe (SubstName (QName a) Type) #

isCoerceVar :: QName a -> Maybe (SubstCoerce (QName a) Type) #

subst :: Name Type -> Type -> QName a -> QName a #

substs :: [(Name Type, Type)] -> QName a -> QName a #

ForallPattern (Subst Type) e => Subst Type (Pattern_ e) Source # 
Instance details

Defined in Disco.AST.Generic

ForallGuard (Subst Type) e => Subst Type (Guard_ e) Source # 
Instance details

Defined in Disco.AST.Generic

Subst Type (Term_ e) => Subst Type (Binding_ e) Source # 
Instance details

Defined in Disco.AST.Generic

ForallQual (Subst Type) e => Subst Type (Qual_ e) Source # 
Instance details

Defined in Disco.AST.Generic

Methods

isvar :: Qual_ e -> Maybe (SubstName (Qual_ e) Type) #

isCoerceVar :: Qual_ e -> Maybe (SubstCoerce (Qual_ e) Type) #

subst :: Name Type -> Type -> Qual_ e -> Qual_ e #

substs :: [(Name Type, Type)] -> Qual_ e -> Qual_ e #

ForallLink (Subst Type) e => Subst Type (Link_ e) Source # 
Instance details

Defined in Disco.AST.Generic

Methods

isvar :: Link_ e -> Maybe (SubstName (Link_ e) Type) #

isCoerceVar :: Link_ e -> Maybe (SubstCoerce (Link_ e) Type) #

subst :: Name Type -> Type -> Link_ e -> Link_ e #

substs :: [(Name Type, Type)] -> Link_ e -> Link_ e #

(Typeable e, ForallTerm (Subst Type) e, ForallTerm Alpha e) => Subst Type (Term_ e) Source # 
Instance details

Defined in Disco.AST.Generic

Methods

isvar :: Term_ e -> Maybe (SubstName (Term_ e) Type) #

isCoerceVar :: Term_ e -> Maybe (SubstCoerce (Term_ e) Type) #

subst :: Name Type -> Type -> Term_ e -> Term_ e #

substs :: [(Name Type, Type)] -> Term_ e -> Term_ e #

type Rep Type Source # 
Instance details

Defined in Disco.Types

pattern TyVar :: Name Type -> Type Source #

pattern TySkolem :: Name Type -> Type Source #

pattern TyVoid :: Type Source #

pattern TyUnit :: Type Source #

pattern TyBool :: Type Source #

pattern TyProp :: Type Source #

pattern TyN :: Type Source #

pattern TyZ :: Type Source #

pattern TyF :: Type Source #

pattern TyQ :: Type Source #

pattern TyC :: Type Source #

pattern (:->:) :: Type -> Type -> Type infixr 5 Source #

pattern (:*:) :: Type -> Type -> Type infixr 7 Source #

pattern (:+:) :: Type -> Type -> Type infixr 6 Source #

pattern TyList :: Type -> Type Source #

pattern TyBag :: Type -> Type Source #

pattern TySet :: Type -> Type Source #

pattern TyGraph :: Type -> Type Source #

pattern TyMap :: Type -> Type -> Type Source #

pattern TyContainer :: Atom -> Type -> Type Source #

pattern TyUser :: String -> [Type] -> Type Source #

An application of a user-defined type.

pattern TyString :: Type Source #

Quantified types

newtype PolyType Source #

PolyType represents a polymorphic type of the form forall a1 a2 ... an. ty (note, however, that n may be 0, that is, we can have a "trivial" polytype which quantifies zero variables).

Constructors

Forall (Bind [Name Type] Type) 

Instances

Instances details
Data PolyType Source # 
Instance details

Defined in Disco.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PolyType -> c PolyType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PolyType #

toConstr :: PolyType -> Constr #

dataTypeOf :: PolyType -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PolyType) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyType) #

gmapT :: (forall b. Data b => b -> b) -> PolyType -> PolyType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PolyType -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PolyType -> r #

gmapQ :: (forall d. Data d => d -> u) -> PolyType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PolyType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PolyType -> m PolyType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PolyType -> m PolyType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PolyType -> m PolyType #

Show PolyType Source # 
Instance details

Defined in Disco.Types

Generic PolyType Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep PolyType :: Type -> Type #

Methods

from :: PolyType -> Rep PolyType x #

to :: Rep PolyType x -> PolyType #

Alpha PolyType Source # 
Instance details

Defined in Disco.Types

Pretty PolyType Source #

Pretty-print a polytype. Note that we never explicitly print forall; quantification is implicit, as in Haskell.

Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => PolyType -> Sem r Doc Source #

Subst Type PolyType Source # 
Instance details

Defined in Disco.Types

type Rep PolyType Source # 
Instance details

Defined in Disco.Types

type Rep PolyType = D1 ('MetaData "PolyType" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'True) (C1 ('MetaCons "Forall" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Bind [Name Type] Type))))

toPolyType :: Type -> PolyType Source #

Convert a monotype into a trivial polytype that does not quantify over any type variables. If the type can contain free type variables, use closeType instead.

closeType :: Type -> PolyType Source #

Convert a monotype into a polytype by quantifying over all its free type variables.

Type predicates

isNumTy :: Type -> Bool Source #

Check whether a type is a numeric type (N, Z, F, Q, or Zn).

isEmptyTy :: Type -> Bool Source #

Decide whether a type is empty, i.e. uninhabited.

isFiniteTy :: Type -> Bool Source #

Decide whether a type is finite.

isSearchable :: Type -> Bool Source #

Decide whether a type is searchable, i.e. effectively enumerable.

Type substitutions

data Substitution a Source #

A value of type Substitution a is a substitution which maps some set of names (the domain, see dom) to values of type a. Substitutions can be applied to certain terms (see applySubst), replacing any free occurrences of names in the domain with their corresponding values. Thus, substitutions can be thought of as functions of type Term -> Term (for suitable Terms that contain names and values of the right type).

Concretely, substitutions are stored using a Map.

See also Disco.Types, which defines S as an alias for substitutions on types (the most common kind in the disco codebase).

Instances

Instances details
Functor Substitution Source # 
Instance details

Defined in Disco.Subst

Methods

fmap :: (a -> b) -> Substitution a -> Substitution b #

(<$) :: a -> Substitution b -> Substitution a #

Eq a => Eq (Substitution a) Source # 
Instance details

Defined in Disco.Subst

Ord a => Ord (Substitution a) Source # 
Instance details

Defined in Disco.Subst

Show a => Show (Substitution a) Source # 
Instance details

Defined in Disco.Subst

Pretty a => Pretty (Substitution a) Source # 
Instance details

Defined in Disco.Subst

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Substitution a -> Sem r Doc Source #

atomToTypeSubst :: Substitution Atom -> Substitution Type Source #

Convert a substitution on atoms into a substitution on types.

uatomToTypeSubst :: Substitution UAtom -> Substitution Type Source #

Convert a substitution on unifiable atoms into a substitution on types.

Strictness

data Strictness Source #

Strictness represents the strictness (either strict or lazy) of a function application or let-expression.

Constructors

Strict 
Lazy 

Instances

Instances details
Eq Strictness Source # 
Instance details

Defined in Disco.Types

Show Strictness Source # 
Instance details

Defined in Disco.Types

Generic Strictness Source # 
Instance details

Defined in Disco.Types

Associated Types

type Rep Strictness :: Type -> Type #

Alpha Strictness Source # 
Instance details

Defined in Disco.Types

type Rep Strictness Source # 
Instance details

Defined in Disco.Types

type Rep Strictness = D1 ('MetaData "Strictness" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Strict" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lazy" 'PrefixI 'False) (U1 :: Type -> Type))

strictness :: Type -> Strictness Source #

Numeric types are strict; others are lazy.

Utilities

isTyVar :: Type -> Bool Source #

Is this a type variable?

containerVars :: Type -> Set (Name Type) Source #

Return a set of all the free container variables in a type.

countType :: Type -> Maybe Integer Source #

Compute the number of inhabitants of a type. Nothing means the type is countably infinite.

unpair :: Type -> [Type] Source #

Decompose a nested product T1 * (T2 * ( ... )) into a list of types.

type S = Substitution Type Source #

Define S as a substitution on types (the most common kind) for convenience.

data TyDefBody Source #

The definition of a user-defined type contains:

  • The actual names of the type variable arguments used in the definition (we keep these around only to help with pretty-printing)
  • A function representing the body of the definition. It takes a list of type arguments and returns the body of the definition with the type arguments substituted.

We represent type definitions this way (using a function, as opposed to a chunk of abstract syntax) because it makes some things simpler, and we don't particularly need to do anything more complicated.

Constructors

TyDefBody [String] ([Type] -> Type) 

Instances

Instances details
Show TyDefBody Source # 
Instance details

Defined in Disco.Types

Pretty (String, TyDefBody) Source #

Pretty-print a type definition.

Instance details

Defined in Disco.Types

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => (String, TyDefBody) -> Sem r Doc Source #

type TyDefCtx = Map String TyDefBody Source #

A TyDefCtx is a mapping from type names to their corresponding definitions.

HasType class

class HasType t where Source #

A type class for things whose type can be extracted or set.

Minimal complete definition

getType

Methods

getType :: t -> Type Source #

Get the type of a thing.

setType :: Type -> t -> t Source #

Set the type of a thing, when that is possible; the default implementation is for setType to do nothing.

Instances

Instances details
HasType APattern Source # 
Instance details

Defined in Disco.AST.Typed

HasType ABranch Source # 
Instance details

Defined in Disco.AST.Typed

HasType ATerm Source # 
Instance details

Defined in Disco.AST.Typed

HasType DPattern Source # 
Instance details

Defined in Disco.AST.Desugared

HasType DTerm Source # 
Instance details

Defined in Disco.AST.Desugared

Orphan instances

(Ord a, Subst t a) => Subst t (Set a) Source # 
Instance details

Methods

isvar :: Set a -> Maybe (SubstName (Set a) t) #

isCoerceVar :: Set a -> Maybe (SubstCoerce (Set a) t) #

subst :: Name t -> t -> Set a -> Set a #

substs :: [(Name t, t)] -> Set a -> Set a #

(Ord k, Subst t a) => Subst t (Map k a) Source # 
Instance details

Methods

isvar :: Map k a -> Maybe (SubstName (Map k a) t) #

isCoerceVar :: Map k a -> Maybe (SubstCoerce (Map k a) t) #

subst :: Name t -> t -> Map k a -> Map k a #

substs :: [(Name t, t)] -> Map k a -> Map k a #