| Copyright | disco team and contributors |
|---|---|
| Maintainer | byorgey@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Disco.Types.Rules
Description
Disco.Types.Rules defines some generic rules about arity, subtyping, and sorts for disco base types.
Synopsis
- data Variance
- arity :: Con -> [Variance]
- data Qualifier
- bopQual :: BOp -> Qualifier
- type Sort = Set Qualifier
- topSort :: Sort
- data Dir
- other :: Dir -> Dir
- isSubA :: Atom -> Atom -> Bool
- isSubB :: BaseTy -> BaseTy -> Bool
- isDirB :: Dir -> BaseTy -> BaseTy -> Bool
- supertypes :: BaseTy -> [BaseTy]
- subtypes :: BaseTy -> [BaseTy]
- dirtypes :: Dir -> BaseTy -> [BaseTy]
- hasQual :: BaseTy -> Qualifier -> Bool
- hasSort :: BaseTy -> Sort -> Bool
- qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier]
- sortRules :: Con -> Sort -> Maybe [Sort]
- pickSortBaseTy :: Sort -> BaseTy
Arity
A particular type argument can be either co- or contravariant with respect to subtyping.
arity :: Con -> [Variance] Source #
The arity of a type constructor is a list of variances, expressing both how many type arguments the constructor takes, and the variance of each argument. This is used to decompose subtyping constraints.
For example, arity CArr = [Contra, Co] since function arrow is
contravariant in its first argument and covariant in its second.
That is, S1 -> T1 S2 - T2 (<: means "is a subtype of") if
and only if S2 <: S1 and T1 <: T2.
Qualifiers
A "qualifier" is kind of like a type class in Haskell; but unlike
Haskell, disco users cannot define their own. Rather, there is a
finite fixed list of qualifiers supported by disco. For example,
QSub denotes types which support a subtraction operation. Each
qualifier corresponds to a set of types which satisfy it (see
hasQual and qualRules).
These qualifiers generally arise from uses of various operations.
For example, the expression \x y. x - y would be inferred to
have a type a -> a -> a [subtractive a], that is, a function of
type a -> a -> a where a is any type that supports
subtraction.
These qualifiers can appear in a CQual constraint; see
Disco.Typecheck.Constraint.
Constructors
| QNum | Numeric, i.e. a semiring supporting + and * |
| QSub | Subtractive, i.e. supports - |
| QDiv | Divisive, i.e. supports / |
| QCmp | Comparable, i.e. supports decidable ordering/comparison (see Note [QCmp]) |
| QEnum | Enumerable, i.e. supports ellipsis notation [x .. y] |
| QBool | Boolean, i.e. supports and, or, not (Bool or Prop) |
| QBasic | Things that do not involve Prop. |
| QSimple | Things for which we can derive a *Haskell* Ord instance |
Instances
bopQual :: BOp -> Qualifier Source #
A helper function that returns the appropriate qualifier for a binary arithmetic operation.
Sorts
type Sort = Set Qualifier Source #
A Sort represents a set of qualifiers, and also represents a
set of types (in general, the intersection of the sets
corresponding to the qualifiers).
Subtyping rules
A "direction" for the subtyping relation (either subtype or supertype).
isSubA :: Atom -> Atom -> Bool Source #
Check whether one atomic type is a subtype of the other. Returns
True if either they are equal, or if they are base types and
isSubB returns true.
isDirB :: Dir -> BaseTy -> BaseTy -> Bool Source #
Check whether one base type is a sub- or supertype of another.
supertypes :: BaseTy -> [BaseTy] Source #
List all the supertypes of a given base type.
Qualifier and sort rules
hasQual :: BaseTy -> Qualifier -> Bool Source #
Check whether a given base type satisfies a qualifier.
hasSort :: BaseTy -> Sort -> Bool Source #
Check whether a base type has a certain sort, which simply amounts to whether it satisfies every qualifier in the sort.
qualRules :: Con -> Qualifier -> Maybe [Maybe Qualifier] Source #
Given a constructor T and a qualifier we want to hold of a type T t1 t2 ..., return a list of qualifiers that need to hold of t1, t2, ...
sortRules :: Con -> Sort -> Maybe [Sort] Source #
sortRules T s = [s1, ..., sn] means that sort s holds of
type (T t1 ... tn) if and only if s1 t1 ... sn tn.
For now this is just derived directly from qualRules.
This is the arity function described in section 4.1 of Traytel et
al.
pickSortBaseTy :: Sort -> BaseTy Source #
Pick a base type (generally the "simplest") that satisfies a given sort.