Safe Haskell	None
Language	Haskell2010

SubHask.SubType

Contents

Template Haskell

Description

This module defines the subtyping mechanisms used in subhask.

Synopsis

Documentation

class s <: t where Source

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

Methods

embedType_ :: Embed s t Source

Instances

(<:) * 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?

Instances

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

data family Embed s t 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.

Instances

data Embed * = Embed0 { unEmbed0 :: s -> t } Source
data Embed (ka -> kb -> *) = Embed2 { unEmbed2 :: forall a b. s a b -> t a b } Source
data Embed (ka -> *) = Embed1 { unEmbed1 :: forall a. s a -> t a } Source

embedType :: s <: t => s -> t Source

embedType1 :: s <: t => s a -> t a Source

embedType2 :: s <: t => s a b -> t a b Source

Template Haskell

mkSubtype :: Q Type -> Q Type -> Name -> Q [Dec] Source

FIXME: This should automatically search for other subtypes that can be inferred from t1 and t2

mkSubtypeInstance :: Type -> Type -> Name -> Dec Source

Calling:

mkSubtypeInstance a b f

generates the following code:

instance a <: b where
   embedType_ = Embed0 f

FIXME: What if the type doesn't have kind *?