-- Copyright 2020-2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

-- | Type-level equivalent of a subset of 'Num'.
--
-- This provides "kindclasses" (actually open type families) with functionality
-- analogous to that provided by the 'Num' typeclass.  Since type-level
-- typeclasses don't exist, instead we translate each would-be method to its
-- own open type family; then "instances" are implemented by providing clauses
-- for each type family "method".  Unfortunately this means we can't group
-- methods into classes that must be implemented all-or-none, but in practice
-- this seems to be okay.

{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Kinds.Num
         ( -- * Conversions
           FromNat, ToInteger

           -- * Arithmetic
         , type (+), type (-), type (*)
         ) where

import Prelude hiding (Integer)

import GHC.TypeNats (Nat)
import qualified GHC.TypeNats as N (type (+), type (-), type (*))

import {-# source #-}  Kinds.Integer (Integer(..))

-- | Type-level numeric conversion from 'Nat'.  Like 'fromInteger' in 'Num'.
type family FromNat (n :: Nat) :: k

type instance FromNat {- k=Nat -} n = n

-- | Type-level conversion to 'Integer'.  Like 'toInteger' in 'Integral'.
type family ToInteger (n :: k) :: Integer

type instance ToInteger {- k=Nat -} n = 'Pos n

-- | Type-level addition "kindclass".
type family (x :: k) + (y :: k) :: k

type instance x + y = (N.+) x y  -- HLint doesn't like qualified TypeOperators.

-- | Type-level subtraction "kindclass".
type family (x :: k) - (y :: k) :: k

type instance x - y = (N.-) x y

-- | Type-level multiplication "kindclass".
type family (x :: k) * (y :: k) :: k

type instance x * y = (N.*) x y