[Haskell-cafe] Mapping over Type Level Literals

[Dominic Steinitz]

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 at steinitz.org
http://idontgetoutmuch.wordpress.com