Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/Fcf.hs
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ module Fcf

, type (+)
, type (-)
, type (Fcf.Data.Nat.*)
, type (Fcf.Class.Num.*)
, type (^)
, type (<=)
, type (>=)
Expand Down Expand Up @@ -180,7 +180,8 @@ import Fcf.Combinators
import Fcf.Data.Bool
import Fcf.Data.Common
import Fcf.Data.List
import Fcf.Data.Nat
import Fcf.Class.Ord
import Fcf.Class.Functor
import Fcf.Class.Bifunctor
import Fcf.Class.Num
import Fcf.Utils
86 changes: 86 additions & 0 deletions src/Fcf/Class/Num.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
{-# 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

1 change: 1 addition & 0 deletions src/Fcf/Data/Nat.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
-- Note that the operators from this module conflict with "GHC.TypeLits" and
-- "GHC.TypeNats".
module Fcf.Data.Nat
{-# DEPRECATED "Use Fcf.Class.Num or Fcf.Class.Ord instead." #-}
( -- * Reexported type
-- | From "GHC.TypeNats".

Expand Down