-- | Type-level hackery.
--
-- This module is used for groups whose parameters are encoded as type-level natural numbers,
-- for example finite cyclic groups, free groups, symmetric groups and braid groups.
--

{-# LANGUAGE PolyKinds, DataKinds, KindSignatures, ScopedTypeVariables, 
             ExistentialQuantification, Rank2Types #-}

module Math.Combinat.TypeLevel 
  ( -- * Proxy
    Proxy(..)
  , proxyUndef
  , proxyOf
  , proxyOf1
  , proxyOf2
  , asProxyTypeOf   -- defined in Data.Proxy
  , asProxyTypeOf1
    -- * Type-level naturals as type arguments
  , typeArg 
  , iTypeArg
    -- * Hiding the type parameter
  , Some (..)
  , withSome , withSomeM
  , selectSome , selectSomeM
  , withSelected , withSelectedM
  )
  where

--------------------------------------------------------------------------------

import Data.Proxy ( Proxy(..) , asProxyTypeOf )
import GHC.TypeLits

import Math.Combinat.Numbers.Primes ( isProbablyPrime )

--------------------------------------------------------------------------------
-- * Proxy

proxyUndef :: Proxy a -> a
proxyUndef :: Proxy a -> a
proxyUndef Proxy a
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"proxyUndef"

proxyOf :: a -> Proxy a
proxyOf :: a -> Proxy a
proxyOf a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

proxyOf1 :: f a -> Proxy a
proxyOf1 :: f a -> Proxy a
proxyOf1 f a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

proxyOf2 :: g (f a) -> Proxy a
proxyOf2 :: g (f a) -> Proxy a
proxyOf2 g (f a)
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

asProxyTypeOf1 :: f a -> Proxy a -> f a 
asProxyTypeOf1 :: f a -> Proxy a -> f a
asProxyTypeOf1 f a
y Proxy a
_ = f a
y

--------------------------------------------------------------------------------
-- * Type-level naturals as type arguments

typeArg :: KnownNat n => f (n :: Nat) -> Integer
typeArg :: f n -> Integer
typeArg = Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> (f n -> Proxy n) -> f n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f n -> Proxy n
forall k (f :: k -> *) (a :: k). f a -> Proxy a
proxyOf1

iTypeArg :: KnownNat n => f (n :: Nat) -> Int
iTypeArg :: f n -> Int
iTypeArg = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (f n -> Integer) -> f n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
typeArg

--------------------------------------------------------------------------------
-- * Hiding the type parameter

-- | Hide the type parameter of a functor. Example: @Some Braid@
data Some f = forall n. KnownNat n => Some (f n)

-- | Uses the value inside a 'Some'
withSome :: Some f -> (forall n. KnownNat n => f n -> a) -> a
withSome :: Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
withSome Some f
some forall (n :: Nat). KnownNat n => f n -> a
polyFun = case Some f
some of { Some f n
stuff -> f n -> a
forall (n :: Nat). KnownNat n => f n -> a
polyFun f n
stuff }

-- | Monadic version of 'withSome'
withSomeM :: Monad m => Some f -> (forall n. KnownNat n => f n -> m a) -> m a
withSomeM :: Some f -> (forall (n :: Nat). KnownNat n => f n -> m a) -> m a
withSomeM Some f
some forall (n :: Nat). KnownNat n => f n -> m a
polyAct = case Some f
some of { Some f n
stuff -> f n -> m a
forall (n :: Nat). KnownNat n => f n -> m a
polyAct f n
stuff }

-- | Given a polymorphic value, we select at run time the
-- one specified by the second argument
selectSome :: Integral int => (forall n. KnownNat n => f n) -> int -> Some f
selectSome :: (forall (n :: Nat). KnownNat n => f n) -> int -> Some f
selectSome forall (n :: Nat). KnownNat n => f n
poly int
n = case Integer -> Maybe SomeNat
someNatVal (int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral int
n :: Integer) of
  Maybe SomeNat
Nothing   -> [Char] -> Some f
forall a. HasCallStack => [Char] -> a
error [Char]
"selectSome: not a natural number"
  Just SomeNat
snat -> case SomeNat
snat of
    SomeNat Proxy n
pxy -> f n -> Some f
forall (f :: Nat -> *) (n :: Nat). KnownNat n => f n -> Some f
Some (f n -> Proxy n -> f n
forall k (f :: k -> *) (a :: k). f a -> Proxy a -> f a
asProxyTypeOf1 f n
forall (n :: Nat). KnownNat n => f n
poly Proxy n
pxy)

-- | Monadic version of 'selectSome'
selectSomeM :: forall m f int. (Integral int, Monad m) => (forall n. KnownNat n => m (f n)) -> int -> m (Some f)
selectSomeM :: (forall (n :: Nat). KnownNat n => m (f n)) -> int -> m (Some f)
selectSomeM forall (n :: Nat). KnownNat n => m (f n)
runPoly int
n = case Integer -> Maybe SomeNat
someNatVal (int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral int
n :: Integer) of
  Maybe SomeNat
Nothing   -> [Char] -> m (Some f)
forall a. HasCallStack => [Char] -> a
error [Char]
"selectSomeM: not a natural number"
  Just SomeNat
snat -> case SomeNat
snat of
    SomeNat Proxy n
pxy -> do
      f n
poly <- m (f n)
forall (n :: Nat). KnownNat n => m (f n)
runPoly 
      Some f -> m (Some f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Some f -> m (Some f)) -> Some f -> m (Some f)
forall a b. (a -> b) -> a -> b
$ f n -> Some f
forall (f :: Nat -> *) (n :: Nat). KnownNat n => f n -> Some f
Some (f n -> Proxy n -> f n
forall k (f :: k -> *) (a :: k). f a -> Proxy a -> f a
asProxyTypeOf1 f n
poly Proxy n
pxy)

-- | Combination of 'selectSome' and 'withSome': we make a temporary structure
-- of the given size, but we immediately consume it.
withSelected 
  :: Integral int 
  => (forall n. KnownNat n => f n -> a) 
  -> (forall n. KnownNat n => f n) 
  -> int 
  -> a
withSelected :: (forall (n :: Nat). KnownNat n => f n -> a)
-> (forall (n :: Nat). KnownNat n => f n) -> int -> a
withSelected forall (n :: Nat). KnownNat n => f n -> a
f forall (n :: Nat). KnownNat n => f n
x int
n = Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
forall (f :: Nat -> *) a.
Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
withSome ((forall (n :: Nat). KnownNat n => f n) -> int -> Some f
forall int (f :: Nat -> *).
Integral int =>
(forall (n :: Nat). KnownNat n => f n) -> int -> Some f
selectSome forall (n :: Nat). KnownNat n => f n
x int
n) forall (n :: Nat). KnownNat n => f n -> a
f

-- | (Half-)monadic version of 'withSelected'
withSelectedM 
  :: forall m f int a. (Integral int, Monad m) 
  => (forall n. KnownNat n => f n -> a) 
  -> (forall n. KnownNat n => m (f n)) 
  -> int 
  -> m a
withSelectedM :: (forall (n :: Nat). KnownNat n => f n -> a)
-> (forall (n :: Nat). KnownNat n => m (f n)) -> int -> m a
withSelectedM forall (n :: Nat). KnownNat n => f n -> a
f forall (n :: Nat). KnownNat n => m (f n)
mx int
n = do 
  Some f
s <- (forall (n :: Nat). KnownNat n => m (f n)) -> int -> m (Some f)
forall (m :: * -> *) (f :: Nat -> *) int.
(Integral int, Monad m) =>
(forall (n :: Nat). KnownNat n => m (f n)) -> int -> m (Some f)
selectSomeM forall (n :: Nat). KnownNat n => m (f n)
mx int
n
  a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
forall (f :: Nat -> *) a.
Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
withSome Some f
s forall (n :: Nat). KnownNat n => f n -> a
f)

--------------------------------------------------------------------------------