[Haskell-cafe] Mapping over Type Level Literals

[Marcin Mrotek]

Now I see that since you don't have a type list anywhere in the return
type, you might try to use type classes:

(works with GHC context stack set to at least one more than the value of N)

-------
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE PolyKinds             #-}

import GHC.TypeLits
import Data.Proxy
import Data.Singletons

data Haar (a :: Nat) (b :: Nat) = Haar { unHaar :: Double -> Double }

haar :: forall n k .
         (KnownNat n, KnownNat k, (2 * k - 1 <=? 2^n - 1) ~ 'True) =>
         Haar n (2 * k - 1)
haar = Haar g where
   g t | (k' - 1) * 2 ** (-n') < t && t <= k'       * 2 ** (-n') =  2
** ((n' - 1) / 2)
       | k'       * 2 ** (-n') < t && t <= (k' + 1) * 2 ** (-n') = -2
** ((n' - 1) / 2)
       | otherwise                                               =  0
     where
         n' = fromIntegral (natVal (Proxy :: Proxy n))
         k' = 2 * (fromIntegral (natVal (Proxy :: Proxy k))) - 1

data Natural = Z | S Natural

type family FromNat n where
    FromNat Z = 0
    FromNat (S n) = 1 + (FromNat n)

type family ToNat i where
    ToNat 0 = Z
    ToNat n = S (ToNat (n - 1))

class Upto n where
    upto :: sing n -> [Integer]

instance Upto Z where
    upto _ = []

instance (KnownNat (FromNat n), Upto n) => Upto (S n)  where
    upto _ = natVal (undefined :: sing (FromNat n)) : upto (undefined :: sing n)

class MapHaar (n :: Nat) (xs :: [(Nat,Nat)]) where
    maphaar :: sing1 n -> sing2 xs -> [[(Double, Double)]]

instance MapHaar n '[] where
    maphaar _ _ = []

instance (Upto (ToNat n), MapHaar n xs, b ~ (2 * k - 1), b <= 2^a - 1,
KnownNat n, KnownNat k, KnownNat a) => MapHaar n ('(a,b) ': xs) where
    maphaar sn _ = h : t
        where l = map (\i -> fromIntegral i / fromIntegral (natVal
sn)) $ upto (undefined :: sing (ToNat n))
              h = map (\x -> (x, unHaar (haar :: Haar a b) x)) l
              t = maphaar sn (undefined :: sing xs)

data instance Sing 100 = S100

foo = maphaar S100 (undefined :: sing '[ '(1,1), '(2,1), '(2,3),
'(3,1), '(3,5), '(3,7)])

-----

Regards,
Marcin