Safe Haskell | None |
---|
A Prelude for type-level programming with type classes
This module includes a partial port of the Prelude as type class predicates and pseudo-syntax for caseif-then-elselambda.
TODO:
- Lambda is useless because the variables are not copied. I need some form of prolog's copy_term.
- Type families don't match if the kinds are too polymorphic, see example for Compose.
- Match and Case need some fine tuning.
- Once the solver for Nat works, implement Num Nat and changes some uses of Integer to Nat
- The GHC Constraint solver doesn't seem to flatten tuple constraints, which sometimes causes it to diverge. For some complex constraints C, C => a converges but ((), C) => a diverges
- module Prelude
- class Lambda1 a c a' | a' c -> a
- class Lambda2 a b c a' b' | a' b' c -> a b
- class Lambda3 a b d c a' b' d' | a' b' d' c -> a b d
- class Lambda4 a b d e c a' b' d' e' | a' b' d' e' c -> a b d e
- type family Lambda :: k
- class If p a b
- class Case a c
- class Case' p b a cs
- data Alternative a b
- class Show a b | a -> b
- class Shows a b c | a b -> c
- class Kind a k' | k -> k', k' -> k
- class (a (==) b) p | a b -> p
- class (a (/=) b) p | a b -> p
- class Compare a b o | a b -> o
- class (a (<) b) p | a b -> p
- class (a (<=) b) p | a b -> p
- class (a (>=) b) p | a b -> p
- class (a (>) b) p | a b -> p
- class Max a b max
- class Min a b min
- class ToEnum i a | k i -> a
- class FromEnum a i | a -> i
- class Succ a b | a -> b
- class Pred a b | a -> b
- class EnumFromTo a b l | a b -> l
- class EnumFromThenTo a c b l | a c b -> l
- class EnumFromToBy a b c l | a b c -> l
- class MinBound a | k -> a
- class MaxBound a | k -> a
- class Not a b | a -> b
- class (a (||) b) c | a b -> c
- class (a (&&) b) c | a b -> c
- class Fst p x | p -> x
- class Snd p x | p -> x
- data StarKind
- class Compose1 f g x z | f g -> x z
- class Compose2 f g x z a | f g -> x z
- class Compose3 f g x z a b | f g -> x z
- class Compose4 f g x z a b c | f g -> x z
- type O = Compose
- type family Compose :: k
- class Partial1 f x y | f x -> y
- class Partial2 f x m y | f x m -> y
- class Partial3 f x m n y | f x m n -> y
- class Partial4 f x m n o y | f x m n o -> y
- type family Partial :: k
- class Apply1 f x
- class Apply2 f x e
- class Apply3 f x e g
- class Apply4 f x e h g
- type family a ($) b :: k
- class Id a b | a -> b, b -> a
- class Flip1 f x y
- class Flip2 f x y m
- class Flip3 f x y m n
- class Flip4 f x y m n o
- type family Flip :: (x -> y -> k) -> y -> x -> k
- class Const1 a b c | a -> c, c -> a
- class Const2 a b c d | a -> d, d -> a
- class Const3 a b c d e | a -> e, e -> a
- class Const4 a b c d e f | a -> f, f -> a
- type family Const :: k
- class Until p f x y
- class ShowsTail a x y | a x -> y
- class Map f l j | f l -> j
- class FoldR f nil list ret | f nil list -> ret
- class FoldL f accum list ret | f accum list -> ret
- class Head l x | l -> x
- class Tail l x | l -> x
- class Last l x | l -> x
- class Init l x | l -> x
- class Null l p | l -> p
- class Length l i | l -> i
- class (l (!!) n) x | l n -> x
- class Drop i l k | i l -> k
- class (a (++) b) c | a b -> c
- type Concat = FoldR ++ `[]`
- class ConcatMap f a b | f a -> b
- class ScanL f x l k | f x l -> k
- class ScanR f x l k | f x l -> k
- class ScanFold1 c x y z | c x y -> z
- type ScanL1 = ScanFold1 ScanL
- type ScanR1 = ScanFold1 ScanR
- type FoldL1 = ScanFold1 FoldL
- type FoldR1 = ScanFold1 FoldR
- class Replicate i a l | i a -> l
- class Take i a b | i a -> b
- class SplitAt i a b
- class TakeWhile f x y
- class DropWhile f x y
- class Span f x y
- class Break f x y
- type And = FoldR && True
- type Or = FoldR || False
- type Any = Compose1 Or `Compose2` Partial1 Map
- type All = Compose1 And `Compose2` Partial1 Map
- class Elem a b p | a b -> p
- type NotElem = Compose1 Not `Compose2` Partial1 Elem
- type Maximum = FoldL1 Max
- class ShowsInteger i x y | i x -> y
- class (a (+) b) sum | a b -> sum
- class AddWithCarry carry a b sum | carry a b -> sum
- class Minus a b dif | a b -> dif
- class Negate a b | a -> b
- class (a (*) b) prod | a b -> prod
- class Signum a b | a -> b
- class Signum' a b | a -> b
- class Abs a b | a -> b
- class Subtract a b dif | a b -> dif
- class Even a p | a -> p
- class Odd a p | a -> p
- class Gcd a b c | a b -> c
- class Gcd' x y z | x y -> z
- class Error a
- class ERROR a
- class AsKindOf a b | a -> b, b -> a
- class Xor a b c | a b -> c, b c -> c, a c -> b
- class (a (.&.) b) c | a b -> c
- class Complement a b | a -> b, b -> a
- class QuotRem a b c | a b -> c
- class QuotRem' a b q r
- class Rem a b c | a b -> c
- class Quot a b c | a b -> c
- class TypeEq' () x y b => TypeEq x y b | x y -> b
- class TypeEq' q x y b | q x y -> b
- class TypeEq'' q x y b | q x y -> b
- module GHC.Prim
- module GHC.TypeLits
- module Prelude.Type.Match
- module Prelude.Type.Integer
- module Prelude.Type.Value
Documentation
module Prelude
Syntax emulation
class Lambda4 a b d e c a' b' d' e' | a' b' d' e' c -> a b d eSource
c => Lambda4 k k1 k2 k3 a b d e c a b d e |
Case
Error ((,) Symbol k) ((,) Symbol k "Case: No matching alternative for" a) => Case k a ([] (Alternative k Constraint)) | |
(Match k a x p, Case' k p b a cs) => Case k a (: (Alternative k Constraint) (--> k Constraint x b) cs) | |
b => Case k a (: (Alternative k Constraint) (Otherwise k Constraint b) ([] (Alternative k Constraint))) |
data Alternative a b Source
Error ((,) Symbol k) ((,) Symbol k "Case: No matching alternative for" a) => Case k a ([] (Alternative k Constraint)) | |
(Match k a x p, Case' k p b a cs) => Case k a (: (Alternative k Constraint) (--> k Constraint x b) cs) | |
b => Case k a (: (Alternative k Constraint) (Otherwise k Constraint b) ([] (Alternative k Constraint))) |
Type Classes
Show
class Shows a b c | a b -> cSource
~ [Symbol] y (Shows Ordering o x) => Shows Ordering o x y | |
If (> Integer i (I 0)) (ShowsInteger i x y) (Negate Integer i j, ShowsInteger j x y', ~ [Symbol] y (: Symbol "-" y')) => Shows Integer i x y | |
Shows Bool False x (: Symbol "False" x) | |
Shows Bool True x (: Symbol "True" x) | |
Shows Symbol a x (: Symbol a x) | |
Shows () () x (: Symbol "()" x) | |
Shows Integer Zeros x (: Symbol "0" x) | |
Shows [k] ([] k) x (: Symbol "[]" x) | |
Shows (Maybe k) (Nothing k) x (: Symbol "Nothing" x) | |
Shows k a x y => Shows (Maybe k) (Just k a) x (: Symbol "Just" y) | |
(Shows k a y z, ShowsTail k l (: Symbol "]" x) y) => Shows [k] (: k a l) x (: Symbol "[" z) | |
Shows k1 a x y => Shows (Either k k1) (Right k k1 a) x (: Symbol "Right" y) | |
Shows k a x y => Shows (Either k k1) (Left k k1 a) x (: Symbol "Left" y) | |
(Shows k a (: Symbol "," y) z, Shows k1 b (: Symbol ")" x) y) => Shows ((,) k k1) ((,) k k1 a b) x (: Symbol "(" z) | |
(Shows k a (: Symbol "," y) z, Shows k1 b (: Symbol "," x) y, Shows k2 c (: Symbol ")" w) x) => Shows ((,,) k k1 k2) ((,,) k k1 k2 a b c) w (: Symbol "(" z) | |
(Shows k a (: Symbol "," y) z, Shows k1 b (: Symbol "," x) y, Shows k2 c (: Symbol "," w) x, Shows k3 d (: Symbol ")" v) w) => Shows ((,,,) k k1 k2 k3) ((,,,) k k1 k2 k3 a b c d) v (: Symbol "(" z) |
Kind
class Kind a k' | k -> k', k' -> kSource
Get kind of a type
Kind Bool a Bool | |
Kind Ordering a Ordering | |
Kind * a StarKind | |
Kind Nat a Nat | |
Kind Symbol a Symbol | |
Kind () () () | |
Kind Integer a Integer | |
Kind [k] ([] k) [k1] | |
Kind (Maybe k) (Nothing k) (Maybe k1) | |
Kind k a k1 => Kind (Maybe k) (Just k a) (Maybe k1) | |
Kind k x k1 => Kind [k] (: k x xs) [k1] | |
Kind k1 a k2 => Kind (Either k k1) (Right k k1 a) (Either l k2) | |
Kind k a k2 => Kind (Either k k1) (Left k k1 a) (Either k2 l) | |
(Kind k a k2, Kind k1 b l) => Kind ((,) k k1) ((,) k k1 a b) (k2, l) | |
(Kind k a k3, Kind k1 b l, Kind k2 c m) => Kind ((,,) k k1 k2) ((,,) k k1 k2 a b c) (k3, l, m) | |
(Kind k a k4, Kind k1 b l, Kind k2 c m, Kind k3 d n) => Kind ((,,,) k k1 k2 k3) ((,,,) k k1 k2 k3 a b c d) (k4, l, m, n) |
Eq
class (a (==) b) p | a b -> pSource
~ Bool p (== Bool a b) => (Bool == a) b p | |
TypeEq Ordering a b p => (Ordering == a) b p | |
TypeEq * a b p => (* == a) b p | |
TypeEq Nat a b p => (Nat == a) b p | |
TypeEq Symbol a b p => (Symbol == a) b p | |
(() == a) b True | |
~ Bool p False => (Integer == i) j p | |
(Integer == Zeros) Zeros True | |
(Integer == Ones) Ones True | |
== Integer i j p => (Integer == (Zero i)) (Zero j) p | |
== Integer i j p => (Integer == (One i)) (One j) p | |
([k] == ([] k)) ([] k) True | |
((Maybe k) == (Nothing k)) (Nothing k) True | |
((Maybe k) == (Nothing k)) (Just k b) False | |
((Maybe k) == (Just k a)) (Nothing k) False | |
== k a b p => ((Maybe k) == (Just k a)) (Just k b) p | |
(== k x y p, == [k] xs zs q, && p q o) => ([k] == (: k x xs)) (: k y ys) o | |
((Either k k1) == (Right k k1 a)) (Left k k1 b) False | |
((Either k k1) == (Left k k1 a)) (Right k k1 b) False | |
== k1 a b p => ((Either k k1) == (Right k k1 a)) (Right k k1 b) p | |
== k1 a b p => ((Either k1 k) == (Left k1 k a)) (Left k1 k b) p | |
(== k a w p, == k1 b x q, && p q o) => (((,) k k1) == ((,) k k1 a b)) ((,) k k1 w x) o | |
(== k a w p, == k1 b x q, == k2 c y r, && p q n, && n r p) => (((,,) k k1 k2) == ((,,) k k1 k2 a b c)) ((,,) k k1 k2 w x y) o | |
(== k a w p, == k1 b x q, == k2 c y r, == k3 d z s, && p q m, && r s n, && m n o) => (((,,,) k k1 k2 k3) == ((,,,) k k1 k2 k3 a b c d)) ((,,,) k k1 k2 k3 w x y z) o |
Ord
class Compare a b o | a b -> oSource
class (a (<) b) p | a b -> pSource
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint LT (~ Bool True p)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ Bool False p)) ([] (Alternative Ordering Constraint))))) => (k < a) b p |
class (a (<=) b) p | a b -> pSource
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint GT (~ Bool False p)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ Bool True p)) ([] (Alternative Ordering Constraint))))) => (k <= a) b p |
class (a (>=) b) p | a b -> pSource
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint LT (~ Bool False p)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ Bool True p)) ([] (Alternative Ordering Constraint))))) => (k >= a) b p |
class (a (>) b) p | a b -> pSource
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint GT (~ Bool True p)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ Bool False p)) ([] (Alternative Ordering Constraint))))) => (k > a) b p |
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint LT (~ k max b)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ k max a)) ([] (Alternative Ordering Constraint))))) => Max k a b max |
(Compare k a b o, Case Ordering o (: (Alternative Ordering Constraint) (--> Ordering Constraint GT (~ k min b)) (: (Alternative Ordering Constraint) (Otherwise Ordering Constraint (~ k min a)) ([] (Alternative Ordering Constraint))))) => Min k a b min |
Enum
class EnumFromTo a b l | a b -> lSource
class EnumFromThenTo a c b l | a c b -> lSource
(FromEnum k a i, FromEnum k c h, FromEnum k b j, EnumFromThenTo Integer i h j k1, Map Integer k (ToEnum k) k1 l) => EnumFromThenTo k a c b l | |
(Minus Integer c a x, EnumFromToBy Integer a b x l) => EnumFromThenTo Integer a c b l |
class EnumFromToBy a b c l | a b c -> lSource
If (< k b a) (~ [k] l ([] k)) (+ k c a d, EnumFromToBy k d b c k1, ~ [k] l (: k a k1)) => EnumFromToBy k a b c l |
Bounded
Primitive kinds
Unit
Maybe
Bool
Ordering
Either
Tuples
Type Literals
Star
Predicates/Constraints
class Compose3 f g x z a b | f g -> x zSource
(g x y, f y z a b) => Compose3 k k1 k2 k3 k4 f g x z a b |
class Compose4 f g x z a b c | f g -> x zSource
(g x y, f y z a b c) => Compose4 k k1 k2 k3 k4 k5 f g x z a b c |
Lists
Integer
class ShowsInteger i x y | i x -> ySource
(QuotRem' i (I 10) q r, ShowsInteger q (: Symbol (Digit r) x) y) => ShowsInteger i x y | |
ShowsInteger Zeros x x |
class AddWithCarry carry a b sum | carry a b -> sumSource
AddWithCarry False Zeros a a | |
AddWithCarry False Ones Zeros Ones | |
AddWithCarry True Zeros Ones Zeros | |
AddWithCarry True Ones a a | |
(~ ((,) Bool Bool) (Add3 carry (IntegerHead a) (IntegerHead b)) ((,) Bool Bool head carry'), ~ Integer (IntegerTail a) a', ~ Integer (IntegerTail b) b', AddWithCarry carry' a' b' tail, ~ Integer sum (IntegerCons head tail)) => AddWithCarry carry a b sum |
class Minus a b dif | a b -> difSource
(Complement Integer b cb, AddWithCarry True a cb dif) => Minus Integer a b dif |
(Signum Integer a s, Case Integer s (: (Alternative Integer Constraint) (--> Integer Constraint Ones (Negate Integer a b)) (: (Alternative Integer Constraint) (Otherwise Integer Constraint (~ Integer a b)) ([] (Alternative Integer Constraint))))) => Abs Integer a b |
Misc functions from the Prelude
Bits
class Xor a b c | a b -> c, b c -> c, a c -> bSource
~ Bool c (Xor Bool a b) => Xor Bool a b c | |
(Xor Bool (IntegerHead a) (IntegerHead b) c, Xor Integer (IntegerTail a) (IntegerTail b) d, ~ Integer e (IntegerCons c d)) => Xor Integer a b e | |
Xor Integer Zeros a a | |
Complement Integer a b => Xor Integer Ones a b |
class (a (.&.) b) c | a b -> cSource
~ k c (.&. k a b) => (k .&. a) b c | |
(Integer .&. Zeros) a Zeros | |
(Integer .&. Ones) a a | |
(.&. Bool False (IntegerHead b) c, .&. Integer a (IntegerTail b) d, ~ Integer e (IntegerCons c d)) => (Integer .&. (Zero a)) b e | |
(.&. Bool True (IntegerHead b) c, .&. Integer a (IntegerTail b) d, ~ Integer e (IntegerCons c d)) => (Integer .&. (One a)) b e |
class Complement a b | a -> b, b -> aSource
Complement Bool False True | |
Complement Bool True False | |
(Complement Bool (IntegerHead a) head, Complement Integer (IntegerTail a) tail, ~ Integer b (IntegerCons head tail)) => Complement Integer a b | |
Complement Integer Zeros Ones | |
Complement Integer Ones Zeros |
Integral
Miscellanous
module GHC.Prim
module GHC.TypeLits
module Prelude.Type.Match
module Prelude.Type.Integer
module Prelude.Type.Value