Copyright | disco team and contributors |
---|---|
Maintainer | byorgey@gmail.com |
Safe Haskell | None |
Language | Haskell2010 |
The Disco.Types module defines the set of types used in the disco language type system, along with various utility functions.
Synopsis
- data BaseTy where
- isCtr :: BaseTy -> Bool
- data Var where
- data Ilk
- pattern U :: Name Type -> Var
- pattern S :: Name Type -> Var
- data Atom where
- isVar :: Atom -> Bool
- isBase :: Atom -> Bool
- isSkolem :: Atom -> Bool
- data UAtom where
- uisVar :: UAtom -> Bool
- uatomToAtom :: UAtom -> Atom
- uatomToEither :: UAtom -> Either BaseTy (Name Type)
- data Con where
- pattern CList :: Con
- pattern CBag :: Con
- pattern CSet :: Con
- data Type where
- pattern TyVar :: Name Type -> Type
- pattern TySkolem :: Name Type -> Type
- pattern TyVoid :: Type
- pattern TyUnit :: Type
- pattern TyBool :: Type
- pattern TyProp :: Type
- pattern TyN :: Type
- pattern TyZ :: Type
- pattern TyF :: Type
- pattern TyQ :: Type
- pattern TyC :: Type
- pattern (:->:) :: Type -> Type -> Type
- pattern (:*:) :: Type -> Type -> Type
- pattern (:+:) :: Type -> Type -> Type
- pattern TyList :: Type -> Type
- pattern TyBag :: Type -> Type
- pattern TySet :: Type -> Type
- pattern TyGraph :: Type -> Type
- pattern TyMap :: Type -> Type -> Type
- pattern TyContainer :: Atom -> Type -> Type
- pattern TyUser :: String -> [Type] -> Type
- pattern TyString :: Type
- newtype PolyType = Forall (Bind [Name Type] Type)
- toPolyType :: Type -> PolyType
- closeType :: Type -> PolyType
- isNumTy :: Type -> Bool
- isEmptyTy :: Type -> Bool
- isFiniteTy :: Type -> Bool
- isSearchable :: Type -> Bool
- data Substitution a
- atomToTypeSubst :: Substitution Atom -> Substitution Type
- uatomToTypeSubst :: Substitution UAtom -> Substitution Type
- data Strictness
- strictness :: Type -> Strictness
- isTyVar :: Type -> Bool
- containerVars :: Type -> Set (Name Type)
- countType :: Type -> Maybe Integer
- unpair :: Type -> [Type]
- type S = Substitution Type
- data TyDefBody = TyDefBody [String] ([Type] -> Type)
- type TyDefCtx = Map String TyDefBody
- class HasType t where
Disco language types
Atomic types
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.
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
Var
represents type variables, that is, variables which stand
for some type.
Instances
Eq Var Source # | |
Data Var Source # | |
Defined in Disco.Types 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 # 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 # | |
Show Var Source # | |
Generic Var Source # | |
Alpha Var Source # | |
Defined in Disco.Types aeq' :: AlphaCtx -> Var -> Var -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Var -> f Var # close :: AlphaCtx -> NamePatFind -> Var -> Var # open :: AlphaCtx -> NthPatFind -> Var -> Var # isPat :: Var -> DisjointSet AnyName # nthPatFind :: Var -> NthPatFind # namePatFind :: Var -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Var -> Var # lfreshen' :: LFresh m => AlphaCtx -> Var -> (Var -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Var -> m (Var, Perm AnyName) # | |
Subst Type Var Source # | |
Subst Atom Var Source # | |
type Rep Var Source # | |
Defined in Disco.Types type Rep Var = D1 ('MetaData "Var" "Disco.Types" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "V" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ilk) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name Type)))) |
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 thatList a
has to beList N
, and hence thata
has to beN
. - 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 fora
. We check this by making up a new skolem variable fora
. 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.
Instances
Eq Ilk Source # | |
Data Ilk Source # | |
Defined in Disco.Types 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 # 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 # | |
Read Ilk Source # | |
Show Ilk Source # | |
Generic Ilk Source # | |
Alpha Ilk Source # | |
Defined in Disco.Types aeq' :: AlphaCtx -> Ilk -> Ilk -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ilk -> f Ilk # close :: AlphaCtx -> NamePatFind -> Ilk -> Ilk # open :: AlphaCtx -> NthPatFind -> Ilk -> Ilk # isPat :: Ilk -> DisjointSet AnyName # nthPatFind :: Ilk -> NthPatFind # namePatFind :: Ilk -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Ilk -> Ilk # lfreshen' :: LFresh m => AlphaCtx -> Ilk -> (Ilk -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Ilk -> m (Ilk, Perm AnyName) # | |
Pretty Ilk Source # | |
Subst Type Ilk Source # | |
Subst Atom Ilk Source # | |
type Rep Ilk 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.
Instances
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.
Instances
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
Compound types, such as functions, product types, and sum types, are an application of a type constructor to one or more argument types.
CArr :: Con | Function type constructor, |
CProd :: Con | Product type constructor, |
CSum :: Con | Sum type constructor, |
CContainer :: Atom -> Con | Container type (list, bag, or set) constructor. Note this
looks like it could contain any |
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
Eq Con Source # | |
Data Con Source # | |
Defined in Disco.Types 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 # 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 # | |
Show Con Source # | |
Generic Con Source # | |
Alpha Con Source # | |
Defined in Disco.Types aeq' :: AlphaCtx -> Con -> Con -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Con -> f Con # close :: AlphaCtx -> NamePatFind -> Con -> Con # open :: AlphaCtx -> NthPatFind -> Con -> Con # isPat :: Con -> DisjointSet AnyName # nthPatFind :: Con -> NthPatFind # namePatFind :: Con -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> Con -> Con # lfreshen' :: LFresh m => AlphaCtx -> Con -> (Con -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Con -> m (Con, Perm AnyName) # | |
Pretty Con Source # | |
Subst Type Con Source # | |
type Rep Con Source # | |
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))))) |
CList
is provided for convenience; it represents a list type
constructor (i.e. List a
).
CBag
is provided for convenience; it represents a bag type
constructor (i.e. Bag a
).
CSet
is provided for convenience; it represents a set type
constructor (i.e. Set a
).
Types
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.
Type
s 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
.
TyAtom :: Atom -> Type | Atomic types (variables and base types), e.g. |
TyCon :: Con -> [Type] -> Type | Application of a type constructor to type arguments, e.g. |
Instances
Quantified types
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).
Instances
Data PolyType Source # | |
Defined in Disco.Types 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 # | |
Generic PolyType Source # | |
Alpha PolyType Source # | |
Defined in Disco.Types aeq' :: AlphaCtx -> PolyType -> PolyType -> Bool # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> PolyType -> f PolyType # close :: AlphaCtx -> NamePatFind -> PolyType -> PolyType # open :: AlphaCtx -> NthPatFind -> PolyType -> PolyType # isPat :: PolyType -> DisjointSet AnyName # nthPatFind :: PolyType -> NthPatFind # namePatFind :: PolyType -> NamePatFind # swaps' :: AlphaCtx -> Perm AnyName -> PolyType -> PolyType # lfreshen' :: LFresh m => AlphaCtx -> PolyType -> (PolyType -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> PolyType -> m (PolyType, Perm AnyName) # | |
Pretty PolyType Source # | Pretty-print a polytype. Note that we never explicitly print
|
Subst Type PolyType Source # | |
type Rep PolyType Source # | |
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
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
Term
s 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
Functor Substitution Source # | |
Defined in Disco.Subst fmap :: (a -> b) -> Substitution a -> Substitution b # (<$) :: a -> Substitution b -> Substitution a # | |
Eq a => Eq (Substitution a) Source # | |
Defined in Disco.Subst (==) :: Substitution a -> Substitution a -> Bool # (/=) :: Substitution a -> Substitution a -> Bool # | |
Ord a => Ord (Substitution a) Source # | |
Defined in Disco.Subst compare :: Substitution a -> Substitution a -> Ordering # (<) :: Substitution a -> Substitution a -> Bool # (<=) :: Substitution a -> Substitution a -> Bool # (>) :: Substitution a -> Substitution a -> Bool # (>=) :: Substitution a -> Substitution a -> Bool # max :: Substitution a -> Substitution a -> Substitution a # min :: Substitution a -> Substitution a -> Substitution a # | |
Show a => Show (Substitution a) Source # | |
Defined in Disco.Subst showsPrec :: Int -> Substitution a -> ShowS # show :: Substitution a -> String # showList :: [Substitution a] -> ShowS # | |
Pretty a => Pretty (Substitution a) 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.
Instances
strictness :: Type -> Strictness Source #
Numeric types are strict; others are lazy.
Utilities
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.
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.
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.
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.