Disco.Types.Qualifiers

Type qualifiers and sorts.

Documentation

data Qualifier

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

Eq Qualifier

Defined in Disco.Types.Qualifiers

Methods

(==) :: Qualifier -> Qualifier -> Bool

(/=) :: Qualifier -> Qualifier -> Bool

Ord Qualifier

Defined in Disco.Types.Qualifiers

Methods

compare :: Qualifier -> Qualifier -> Ordering

(<) :: Qualifier -> Qualifier -> Bool

(<=) :: Qualifier -> Qualifier -> Bool

(>) :: Qualifier -> Qualifier -> Bool

(>=) :: Qualifier -> Qualifier -> Bool

max :: Qualifier -> Qualifier -> Qualifier

min :: Qualifier -> Qualifier -> Qualifier

Show Qualifier

Defined in Disco.Types.Qualifiers

Methods

showsPrec :: Int -> Qualifier -> ShowS

show :: Qualifier -> String

showList :: [Qualifier] -> ShowS

Generic Qualifier

Defined in Disco.Types.Qualifiers

Associated Types

type Rep Qualifier :: Type -> Type

Methods

from :: Qualifier -> Rep Qualifier x

to :: Rep Qualifier x -> Qualifier

Alpha Qualifier

Defined in Disco.Types.Qualifiers

Methods

aeq' :: AlphaCtx -> Qualifier -> Qualifier -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Qualifier -> f Qualifier

close :: AlphaCtx -> NamePatFind -> Qualifier -> Qualifier

open :: AlphaCtx -> NthPatFind -> Qualifier -> Qualifier

isPat :: Qualifier -> DisjointSet AnyName

isTerm :: Qualifier -> All

isEmbed :: Qualifier -> Bool

nthPatFind :: Qualifier -> NthPatFind

namePatFind :: Qualifier -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Qualifier -> Qualifier

lfreshen' :: LFresh m => AlphaCtx -> Qualifier -> (Qualifier -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Qualifier -> m (Qualifier, Perm AnyName)

acompare' :: AlphaCtx -> Qualifier -> Qualifier -> Ordering

Pretty Qualifier

Defined in Disco.Types.Qualifiers

Methods

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

Subst Type Qualifier

Defined in Disco.Types

Methods

isvar :: Qualifier -> Maybe (SubstName Qualifier Type)

isCoerceVar :: Qualifier -> Maybe (SubstCoerce Qualifier Type)

subst :: Name Type -> Type -> Qualifier -> Qualifier

substs :: [(Name Type, Type)] -> Qualifier -> Qualifier

type Rep Qualifier

Defined in Disco.Types.Qualifiers

type Rep Qualifier = D1 ('MetaData "Qualifier" "Disco.Types.Qualifiers" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (((C1 ('MetaCons "QNum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QSub" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "QDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QCmp" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "QEnum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QBool" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "QBasic" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "QSimple" 'PrefixI 'False) (U1 :: Type -> Type))))

decidable* (terminating) comparison.

bopQual :: BOp -> Qualifier

A helper function that returns the appropriate qualifier for a binary arithmetic operation.

type Sort = Set Qualifier

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).

topSort :: Sort

The special sort \(\top\) which includes all types.