-
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
import Data.Proxy
import GHC.TypeLits
data S a = S a (S a)
data T n a = T a deriving (Show)
toProxy :: T n a -> Proxy n
toProxy _ = Proxy
mkT :: KnownNat n => proxy n -> a -> T n a
mkT _ a = T a
useT t@(T a) = fromIntegral (natVal (toProxy t)) + a
*Main> useT $ mkT (Proxy :: Proxy 4) 0.5
4.5
так, то! в то время как космические питоны бороздят просторы динамического варианта, мы храним значения в типах!
Replies (6)
-
@qnikst, Продолжаем разговор:
*Main> useTF $ mkT (Proxy :: Proxy (1 :%% 3)) 0.5
0.8333333333333333
data (:%%) (a::Nat) (b::Nat)
numerator :: T (n :%% m) a -> Proxy n
numerator _ = Proxy
denomenator :: T (n :%% m) a -> Proxy m
denomenator _ = Proxy
useTF :: (KnownNat n, KnownNat m, Fractional a) => T (n :%% m) a -> a
useTF t@(T a) = fromRational (natVal (numerator t) :% natVal (denomenator t)) + a
~
-
@qnikst, спасибо @balodja, с помощью toRational TH и чертовой матери оно работает:
mkFloatProxy :: RealFrac a => a -> Q Exp
mkFloatProxy x = [| Proxy :: Proxy ($(nk a) :%% $(nk b)) |]
where (a :% b) = toRational x
nk x = sigT (litT (numTyLit x)) (ConT $ mkName "Nat")
test = mkT ($(mkFloatProxy pi)) 7.0
