haskell - 在 Haskell 中从 Kind 构造值

Question

我想从一个类型到值如下，但不使用折旧的 DatatypeContexts：

{-# LANGUAGE DataKinds #-}          
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DatatypeContexts #-}   

import Data.Proxy
import GHC.TypeLits

data (KnownNat n) => MagicN n a = MagicN a             
  deriving (Show)                                      

getMagicN :: forall n. (KnownNat n) => MagicN n Integer
getMagicN = MagicN $ natVal (Proxy :: Proxy n)         

MagicN five = getMagicN :: MagicN 5 Integer                     

如果使用这种或其他方法（Peano 数等），我不太担心；要求是能够仅从类型信息中构造值。

谢谢！

Answer 1

您只需要一种更好的方法来约束MagicN' 的第一个参数的种类。{-# LANGUAGE KindSignatures #-}会给你你所需要的。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}

import Data.Proxy
import GHC.TypeLits

data MagicN (n :: Nat) a = MagicN a
  deriving (Show)

其余的都是一样的。

注意：KindSignatures由PolyKinds和隐含TypeFamilies，因此如果您使用后者中的任何一个，则无需显式添加它。