[Haskell-cafe] Mapping over Type Level Literals

11 Sep 2014

      I was playing around with Haar functions and realised I could encode the constraints in the types
...
...
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
...
import GHC.TypeLits
import Data.Proxy
...
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
So now I can do e.g.
...
*Main> unHaar (haar :: Haar 3 7) 0.05
0.0
*Main> unHaar (haar :: Haar 3 6) 0.05
<interactive>:359:9:
    Couldn't match type ‘2 * k0’ with ‘7’
    The type variable ‘k0’ is ambiguous
    Expected type: 'True
      Actual type: ((2 * k0) - 1) <=? ((2 ^ 3) - 1)
    In the first argument of ‘unHaar’, namely ‘(haar :: Haar 3 6)’
    In the expression: unHaar (haar :: Haar 3 6) 0.05
    In an equation for ‘it’: it = unHaar (haar :: Haar 3 6) 0.05
*Main> unHaar (haar :: Haar 3 9) 0.05
<interactive>:360:9:
    Couldn't match type ‘'False’ with ‘'True’
    Expected type: 'True
      Actual type: ((2 * 5) - 1) <=? ((2 ^ 3) - 1)
    In the first argument of ‘unHaar’, namely ‘(haar :: Haar 3 9)’
    In the expression: unHaar (haar :: Haar 3 9) 0.05
    In an equation for ‘it’: it = unHaar (haar :: Haar 3 9) 0.05
*Main>
So errors get rejected at compilation time as one would like and with moderately informative error messages.

But now of course I would like to map over n and k but these are at the type level. Can this be done? I imagine unsafeCoerce would have to come into it somewhere.

Dominic Steinitz
dominic@steinitz.org
http://idontgetoutmuch.wordpress.com