ddc-core- Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe




equivT :: Ord n => EnvT n -> Type n -> Type n -> Bool Source #

Check equivalence of types.

Checks equivalence up to alpha-renaming, as well as crushing of effects and trimming of closures.

  • Return False if we find any free variables.
  • We assume the types are well-kinded, so that the type annotations on bound variables match the binders. If this is not the case then you get an indeterminate result.

equivWithBindsT Source #


:: Ord n 
=> EnvT n

Environment of types.

-> [Bind n]

Stack of binders for first type.

-> [Bind n]

Stack of binders for second type.

-> Type n

First type to compare.

-> Type n

Second type to compare.

-> Bool 

Like equivT but take the initial stacks of type binders.

equivTyCon :: Eq n => TyCon n -> TyCon n -> Bool Source #

Check if two TyCons are equivalent. We need to handle TyConBound specially incase it's kind isn't attached,

crushHeadT :: Ord n => EnvT n -> Type n -> Type n Source #

Crush effects in the given type.

crushSomeT :: Ord n => EnvT n -> Type n -> Type n Source #

Crush compound effects and closure terms. We check for a crushable term before calling crushT because that function will recursively crush the components. As equivT is already recursive, we don't want a doubly-recursive function that tries to re-crush the same non-crushable type over and over.

crushEffect :: Ord n => EnvT n -> Effect n -> Effect n Source #

Crush compound effect terms into their components.

For example, crushing DeepRead (List r1 (Int r2)) yields (Read r1 + Read r2).