first-class-families/src/Fcf/Class/Num.hs at 0a64bed7986c8bbffcd0bbcdecf880f5e651ffa2 · Lysxia/first-class-families · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
{-# LANGUAGE
    CPP,
    DataKinds,
    PolyKinds,
    TypeFamilies,
    TypeOperators,
    UndecidableInstances #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif


-- | Numeric operations.
module Fcf.Class.Num
  ( -- * Pure type families
    -- | Nicer to use when applied explicitly.
    type (:+)
  , type (:-)
  , type (:*)
  , type (:^)

    -- * First-class families
    -- | Can be composed and passed to higher-order functions.
  , type (+)
  , type (-)
  , type (Fcf.Class.Num.*)
  , type (^)
  ) where

import Fcf.Core (Exp, Eval)

#if __GLASGOW_HASKELL__ >= 802
import qualified GHC.TypeLits as TL
#endif

-- | Type-level addition.
--
-- This is the fcf-encoding of @(':+')@.
-- To define a new addition, add type instances to @(':+')@.
data (+) :: a -> a -> Exp a
type instance Eval (x + y) = x :+ y

-- | Type-level semigroup composition @('Data.Semigroup.<>')@.
type family (:+) (x :: a) (y :: a) :: a

type instance (:+) (a :: TL.Nat) (b :: TL.Nat)= a TL.+ b

-- | Type-level subtraction.
--
-- This is the fcf-encoding of @(':-')@.
-- To define a new subtraction, add type instances to @(':-')@.
data (-) :: a -> a -> Exp a
type instance Eval (x - y) = x :- y

-- | Type-level subtraction.
type family (:-) (x :: a) (y :: a) :: a

type instance (:-) (a :: TL.Nat) (b :: TL.Nat) = a TL.- b

-- | Type-level multiplication.
--
-- This is the fcf-encoding of @('Fcf.Data.Nat.*')@.
-- To define a new multiplication, add type instances to @('Fcf.Data.Nat.*')@.
data (*) :: a -> a -> Exp a

type instance Eval (x Fcf.Class.Num.* y) = x :* y

-- | Type-level multiplication.
type family (:*) (x :: a) (y :: a) :: a

type instance (:*) (a :: TL.Nat) (b :: TL.Nat) = a TL.* b


-- | Type-level exponentiation.
--
-- This is the fcf-encoding of @('^')@.
-- To define a new exponentiation, add type instances to @('^')@.
data (^) :: a -> b -> Exp a
type instance Eval (x ^ y) = x :^ y

-- | Type-level exponentiation.
type family (:^) (x :: a) (y :: b) :: a

type instance (:^) (a :: TL.Nat) (b :: TL.Nat) = a TL.^ b