-- | 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 :: forall a. Proxy a -> a
proxyUndef Proxy a
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"proxyUndef"

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

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

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

asProxyTypeOf1 :: f a -> Proxy a -> f a 
asProxyTypeOf1 :: forall {k} (f :: k -> *) (a :: k). 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 :: forall (n :: Nat) (f :: Nat -> *). KnownNat n => f n -> Integer
typeArg = forall (n :: Nat) (f :: Nat -> *). KnownNat n => f n -> Integer
natVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). f a -> Proxy a
proxyOf1

iTypeArg :: KnownNat n => f (n :: Nat) -> Int
iTypeArg :: forall (n :: Nat) (f :: Nat -> *). KnownNat n => f n -> Int
iTypeArg = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (f :: Nat -> *). KnownNat n => f 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 :: forall (f :: Nat -> *) a.
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 -> 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 :: forall (m :: * -> *) (f :: Nat -> *) a.
Monad m =>
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 -> 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 int (f :: Nat -> *).
Integral int =>
(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 (forall a b. (Integral a, Num b) => a -> b
fromIntegral int
n :: Integer) of
  Maybe SomeNat
Nothing   -> forall a. HasCallStack => [Char] -> a
error [Char]
"selectSome: not a natural number"
  Just SomeNat
snat -> case SomeNat
snat of
    SomeNat Proxy n
pxy -> forall (f :: Nat -> *) (n :: Nat). KnownNat n => f n -> Some f
Some (forall {k} (f :: k -> *) (a :: k). f a -> Proxy a -> f a
asProxyTypeOf1 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 (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)
runPoly int
n = case Integer -> Maybe SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral int
n :: Integer) of
  Maybe SomeNat
Nothing   -> 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 <- forall (n :: Nat). KnownNat n => m (f n)
runPoly 
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: Nat -> *) (n :: Nat). KnownNat n => f n -> Some f
Some (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 int (f :: Nat -> *) a.
Integral int =>
(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 = forall (f :: Nat -> *) a.
Some f -> (forall (n :: Nat). KnownNat n => f n -> a) -> a
withSome (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 (m :: * -> *) (f :: Nat -> *) int a.
(Integral int, Monad m) =>
(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 (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
  forall (m :: * -> *) a. Monad m => a -> m a
return (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)

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