Type-class overloaded functions: second-order typeclass programming with backtracking
- type Fractionals = Float :*: (Double :*: HNil)
- type Nums = Int :*: (Integer :*: (AllOf Fractionals :*: HNil))
- type Ords = Bool :*: (Char :*: (AllOf Nums :*: HNil))
- type Eqs = AllOf (TypeCl OpenEqs) :*: (AllOfBut Ords Fractionals :*: HNil)
- data OpenEqs
- data RusselC
- type Russel = AllOfBut () (TypeCl RusselC) :*: HNil
- data AllOf x
- data AllOfBut x y
- data TypeCl x
- class TypeCls l x r | l x -> r
- data Member tl
- class MemApp bf t x r | bf t x -> r
- data MemCase2 h t x
- class GFN n f a pred | n f a -> pred
- data Otherwise
- newtype GFn f = GFn f
- newtype GFnA n f = GFnA f
- newtype GFnTest n f flag = GFnTest f
- data IsAnEq = IsAnEq
- data PairOf t
- data ApproxEq = ApproxEq
- data ApproxEq' = ApproxEq'
- data HNil = HNil
- data a :*: b = a :*: b
- data HTrue
- data HFalse
- data Z = Z
- newtype S n = S n
- class TypeCast a b | a -> b, b -> a where
- typeCast :: a -> b
- class TypeCast' t a b | t a -> b, t b -> a where
- typeCast' :: t -> a -> b
- class TypeCast'' t a b | t a -> b, t b -> a where
- typeCast'' :: t -> a -> b
- class TypeEq x y b | x y -> b
- class Apply f a r | f a -> r where
- apply :: f -> a -> r
Documentation
The Fractionals, Nums and Ords above are closed. But Eqs is open (i.e., extensible), due to the following:
Why we call Nums etc. a type class rather than a type set? The following does not work: type synonyms can't be recursive.
type Russel = AllOfBut () Russel :*: HNil
But the more elaborate version does, with the expected result:
class TypeCls l x r | l x -> rSource
Classifies if the type x belongs to the open class labeled l The result r is either HTrue or HFalse
Deciding the membership in a closed class, specified by enumeration, union and difference
GFN Z IsAnEq a (Member Eqs) | Each case of a 2-poly function is defined by two instances, of GFN and or Apply classes. |
GFN Z ApproxEq' (x, x) (PairOf (Member Nums)) | |
GFN Z ApproxEq (x, x) (PairOf (Member Fractionals)) | |
(TypeEq h x bf, MemApp bf t x r) => Apply (Member (:*: h t)) x r | |
(Apply (Member exc) x bf, Apply (MemCase2 h t x) bf r) => Apply (Member (:*: (AllOfBut h exc) t)) x r | |
(Apply (Member h) x bf, MemApp bf t x r) => Apply (Member (:*: (AllOf h) t)) x r | |
Apply (Member HNil) x HFalse | |
TypeCls l x r => Apply (Member (TypeCl l)) x r | |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) |
we avoid defining a new class like MemApp above. I guess, after Apply, we don't need a single class ever?
class GFN n f a pred | n f a -> predSource
A type class for instance guards and back-tracking Here, pred and f are labels and n is of a kind numeral.
TypeCast pred Otherwise => GFN n ApproxEq' a pred | |
TypeCast pred Otherwise => GFN n ApproxEq a pred | |
TypeCast pred Otherwise => GFN n IsAnEq a pred | the default instance |
GFN Z IsAnEq a (Member Eqs) | Each case of a 2-poly function is defined by two instances, of GFN and or Apply classes. |
GFN Z ApproxEq' (x, x) (PairOf (Member Nums)) | |
GFN Z ApproxEq (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) IsAnEq (x, y) Otherwise | Augment the above function, to test for pairs of Eqs We could have added an instance to TypeCls OpenEqs above. But we wish to show off the recursive invocation of a second-order polymorphic function |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) |
The guard that always succeeds (cf. otherwise
in Haskell)
GFn f |
GFnA f |
Apply (GFnA n ApproxEq') a Bool | |
Apply (GFnA n ApproxEq) a Bool | |
Apply (GFnA n IsAnEq) a Bool | |
Apply (GFnA Z IsAnEq) a Bool | |
(Apply (GFn ApproxEq) (x, x) Bool, Eq x) => Apply (GFnA (S (S (S Z))) ApproxEq) ((x, x), (x, x)) Bool | |
Eq x => Apply (GFnA (S (S Z)) ApproxEq) (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA (S Z) ApproxEq') (x, x) Bool | |
(Num x, Ord x) => Apply (GFnA (S Z) ApproxEq) (x, x) Bool | |
(Apply (GFn IsAnEq) x Bool, Apply (GFn IsAnEq) y Bool) => Apply (GFnA (S Z) IsAnEq) (x, y) Bool | |
(Num x, Ord x) => Apply (GFnA Z ApproxEq') (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA Z ApproxEq) (x, x) Bool |
A generic function that tests if its argument is a member of Eqs
TypeCast pred Otherwise => GFN n IsAnEq a pred | the default instance |
GFN Z IsAnEq a (Member Eqs) | Each case of a 2-poly function is defined by two instances, of GFN and or Apply classes. |
GFN (S Z) IsAnEq (x, y) Otherwise | Augment the above function, to test for pairs of Eqs We could have added an instance to TypeCls OpenEqs above. But we wish to show off the recursive invocation of a second-order polymorphic function |
Apply (GFnA n IsAnEq) a Bool | |
Apply (GFnA Z IsAnEq) a Bool | |
(Apply (GFn IsAnEq) x Bool, Apply (GFn IsAnEq) y Bool) => Apply (GFnA (S Z) IsAnEq) (x, y) Bool |
The main test: approximate equality. See the article for the description.
GFN Z ApproxEq' (x, x) (PairOf (Member Nums)) | |
GFN Z ApproxEq (x, x) (PairOf (Member Fractionals)) | |
TypeCast r HFalse => Apply (PairOf t) x r | |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) | |
Apply t x r => Apply (PairOf t) (x, x) r |
TypeCast pred Otherwise => GFN n ApproxEq a pred | |
GFN Z ApproxEq (x, x) (PairOf (Member Fractionals)) | |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) | |
Apply (GFnA n ApproxEq) a Bool | |
(Apply (GFn ApproxEq) (x, x) Bool, Eq x) => Apply (GFnA (S (S (S Z))) ApproxEq) ((x, x), (x, x)) Bool | |
Eq x => Apply (GFnA (S (S Z)) ApproxEq) (x, x) Bool | |
(Num x, Ord x) => Apply (GFnA (S Z) ApproxEq) (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA Z ApproxEq) (x, x) Bool |
TypeCast pred Otherwise => GFN n ApproxEq' a pred | |
GFN Z ApproxEq' (x, x) (PairOf (Member Nums)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
Apply (GFnA n ApproxEq') a Bool | |
(Fractional x, Ord x) => Apply (GFnA (S Z) ApproxEq') (x, x) Bool | |
(Num x, Ord x) => Apply (GFnA Z ApproxEq') (x, x) Bool |
a :*: b |
GFN Z IsAnEq a (Member Eqs) | Each case of a 2-poly function is defined by two instances, of GFN and or Apply classes. |
GFN Z ApproxEq' (x, x) (PairOf (Member Nums)) | |
GFN Z ApproxEq (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) IsAnEq (x, y) Otherwise | Augment the above function, to test for pairs of Eqs We could have added an instance to TypeCls OpenEqs above. But we wish to show off the recursive invocation of a second-order polymorphic function |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) | |
Apply (GFnA Z IsAnEq) a Bool | |
(Apply (GFn ApproxEq) (x, x) Bool, Eq x) => Apply (GFnA (S (S (S Z))) ApproxEq) ((x, x), (x, x)) Bool | |
Eq x => Apply (GFnA (S (S Z)) ApproxEq) (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA (S Z) ApproxEq') (x, x) Bool | |
(Num x, Ord x) => Apply (GFnA (S Z) ApproxEq) (x, x) Bool | |
(Apply (GFn IsAnEq) x Bool, Apply (GFn IsAnEq) y Bool) => Apply (GFnA (S Z) IsAnEq) (x, y) Bool | |
(Num x, Ord x) => Apply (GFnA Z ApproxEq') (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA Z ApproxEq) (x, x) Bool |
S n |
GFN (S Z) IsAnEq (x, y) Otherwise | Augment the above function, to test for pairs of Eqs We could have added an instance to TypeCls OpenEqs above. But we wish to show off the recursive invocation of a second-order polymorphic function |
GFN (S (S (S Z))) ApproxEq ((x, x), (x, x)) (PairOf (PairOf (Member Nums))) | |
GFN (S (S Z)) ApproxEq (x, x) (PairOf (Member Eqs)) | |
GFN (S Z) ApproxEq' (x, x) (PairOf (Member Fractionals)) | |
GFN (S Z) ApproxEq (x, x) (PairOf (Member Nums)) | |
(Apply (GFn ApproxEq) (x, x) Bool, Eq x) => Apply (GFnA (S (S (S Z))) ApproxEq) ((x, x), (x, x)) Bool | |
Eq x => Apply (GFnA (S (S Z)) ApproxEq) (x, x) Bool | |
(Fractional x, Ord x) => Apply (GFnA (S Z) ApproxEq') (x, x) Bool | |
(Num x, Ord x) => Apply (GFnA (S Z) ApproxEq) (x, x) Bool | |
(Apply (GFn IsAnEq) x Bool, Apply (GFn IsAnEq) y Bool) => Apply (GFnA (S Z) IsAnEq) (x, y) Bool |
class TypeCast' t a b | t a -> b, t b -> a whereSource
TypeCast'' t a b => TypeCast' t a b |
class TypeCast'' t a b | t a -> b, t b -> a whereSource
typeCast'' :: t -> a -> bSource
TypeCast'' () a a |
class Apply f a r | f a -> r whereSource