Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module defines the subtyping mechanisms used in subhask.
Documentation
We use `s <: t` to denote that s is s subtype of t. The "embedType" function must be s homomorphism from s to t.
class (Sup s t t, Sup t s t) => (s :: k) <: (t :: k) where
embedType_ :: Embed s t Source
(<:) * a a Source | |
(<:) * a (ProofOf * Hask a) Source | |
(Ord_ a, Ord_ b) => (<:) * (Hask (ProofOf * (IncreasingT Hask) a) (ProofOf * (IncreasingT Hask) b)) (IncreasingT Hask a b) Source | |
(<:) (* -> * -> *) Polynomial_ Hask Source | |
(<:) (* -> * -> *) (+>) (->) Source | |
(<:) (k1 -> k2 -> *) a a Source | |
(<:) (k1 -> *) a a Source | |
(<:) (* -> * -> *) subcat cat => (<:) (* -> * -> *) (IncreasingT subcat) cat Source | |
(<:) (* -> * -> *) subcat cat => (<:) (* -> * -> *) (MonT subcat) cat Source | |
(<:) (* -> * -> *) (Diff n) (->) Source | |
(<:) (* -> * -> *) (Diff 0) (->) Source | |
(<:) (* -> * -> *) (Diff 1) (Diff 0) Source | |
(<:) (* -> * -> *) (Diff 2) (Diff 0) Source | |
(<:) (* -> * -> *) (Diff 2) (Diff 1) Source | |
(<:) (* -> * -> *) subcat cat => (<:) (* -> * -> *) (ConstrainedT xs subcat) cat Source | |
(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (BijectiveT k k subcat) cat Source | |
(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (SurjectiveT k k subcat) cat Source | |
(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (InjectiveT k k subcat) cat Source |
class Sup s t u | s t -> u Source
Subtypes are partially ordered. Unfortunately, there's no way to use the machinery of the POrd/Lattice classes. The Sup type family is a promotion of the "sup" function to the type level.
It must obey the laws:
Sup a b c <===> ( a <: c, b <: c )
Sub a b c <===> Sup b a c
And there is no smaller value of "c" that can be used instead.
FIXME: it would be nicer if this were a type family; is that possible?
Sup k s s s Source | |
Sup * a (ProofOf k cat a) (ProofOf k cat a) Source | |
Sup * (ProofOf k cat a) a (ProofOf k cat a) Source | |
Sup (* -> * -> *) (->) (+>) (->) Source | |
Sup (* -> * -> *) Hask Polynomial_ Hask Source | |
Sup (* -> * -> *) Polynomial_ Hask Hask Source | |
Sup (* -> * -> *) (+>) (->) (->) Source | |
Sup (* -> * -> *) (->) (Diff n) (->) Source | |
Sup (* -> * -> *) b a c => Sup (* -> * -> *) a (IncreasingT b) c Source | |
Sup (* -> * -> *) b a c => Sup (* -> * -> *) a (MonT b) c Source | |
Sup (* -> * -> *) b a c => Sup (* -> * -> *) a (ConstrainedT xs b) c Source | |
Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (BijectiveT k k b) c Source | |
Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (SurjectiveT k k b) c Source | |
Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (InjectiveT k k b) c Source | |
Sup (* -> * -> *) a b c => Sup (* -> * -> *) (IncreasingT a) b c Source | |
Sup (* -> * -> *) a b c => Sup (* -> * -> *) (MonT a) b c Source | |
Sup (* -> * -> *) (Diff n) (->) (->) Source | |
Sup (* -> * -> *) (Diff 0) (Diff 1) (Diff 0) Source | |
Sup (* -> * -> *) (Diff 0) (Diff 2) (Diff 0) Source | |
Sup (* -> * -> *) (Diff 1) (Diff 0) (Diff 0) Source | |
Sup (* -> * -> *) (Diff 1) (Diff 2) (Diff 1) Source | |
Sup (* -> * -> *) (Diff 2) (Diff 0) (Diff 0) Source | |
Sup (* -> * -> *) (Diff 2) (Diff 1) (Diff 1) Source | |
Sup (* -> * -> *) a b c => Sup (* -> * -> *) (ConstrainedT xs a) b c Source | |
Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (BijectiveT k k a) b c Source | |
Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (SurjectiveT k k a) b c Source | |
Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (InjectiveT k k a) b c Source |
This data type is a huge hack to work around some unimplemented features in the type system. In particular, we want to be able to declare any type constructor to be a subtype of any other type constructor. The main use case is for making subcategories use the same subtyping mechanism as other types.
FIXME: replace this data family with a system based on type families; everything I've tried so far requires injective types or foralls in constraints.
embedType1 :: s <: t => s a -> t a Source
embedType2 :: s <: t => s a b -> t a b Source