• Haskell typefun {-# 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, теперь охота тоже самое, но для Fractional..
  • @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, задавать проксю таким образом не очень удобно, вот нужно мне точку pi задать и что делать? нужно решить и этот вопрос
  • @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
  • @qnikst, 134/100
  • @rkit, а если точнее, а если √π? не-не-не уж делать так чтоб удобно