我发现了两种在运行时将Integer提升为Nat(或KnownNat，我还没有得到区分)的方法，要么使用TypeLits和Proxy(Data.Proxy和GHC.TypeLits)，要么使用Singleton(Data.Singletons)。在下面的代码中，你可以看到这两种方法中的每一种是如何使用的：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main where
import Prelude hiding (replicate)
import Data.Proxy (Proxy(Proxy))
import Data.Monoid ((<>))
import Data.Singletons (SomeSing(..), toSing)
import GHC.TypeLits
import Data.Singletons.TypeLits
import Data.Vector.Sized (Vector, replicate)
main :: IO ()
main = playingWithTypes 8
playingWithTypes :: Integer -> IO ()
playingWithTypes nn = do
case someNatVal nn of
Just (SomeNat (proxy :: Proxy n)) -> do
-- let (num :: Integer) = natVal proxy
-- putStrLn $ "Some num: " <> show num
putStrLn $ "Some vector: " <> show (replicate 5 :: Vector n Int)
Nothing -> putStrLn "There's no number, the integer was not a natural number"
case (toSing nn :: SomeSing Nat) of
SomeSing (SNat :: Sing n) -> do
-- let (num :: Integer) = natVal (Proxy :: Proxy n)
-- putStrLn $ "Some num: " <> show num
putStrLn $ "Some vector: " <> show (replicate 5 :: Vector n Int)
TypeLits的文档指出，开发人员不应该使用它，但Singleton并没有捕捉到给定Integer不是自然数的情况(即，运行playingWithTypes 8运行时没有错误，但当我们试图从非自然数创建Singleton时，playingWithTypes (-2)失败)。
那么，将Integer提升为Nat的"标准"方式是什么？或者，使用TypeLits和Proxy或Singleton进行推广的最佳方法是什么？
Nat(或KnownNat，我还没有得到区别)
Nat是一类类型级的自然数。它没有术语级别的居民。其思想是GHC将任何自然数提升到类型级别，并赋予其类型Nat。
KnownNat是对Nat类事物的约束，其实现见证了如何将Nat类事物转换为术语级Integer。GHC自动为所有类型级别的Nat1居民创建KnownNat的实例。
也就是说，即使每个n :: Nat(读取类型为Nat的n)上都有一个KnownNat实例1，您仍然需要写出约束。
我找到了两种方法来将
Integer提升为Nat
你真的吗？归根结底，Nat在今天的GHC中简直是神奇的。singletons利用了同样的魔力。在引擎盖下，它使用someNatVal。
那么，将
Integer提升为Nat的"标准"方法是什么？或者，使用GHC.TypeLits和Proxy，或者单体，最好的推广方法是什么？
没有标准的方法。我的观点是：当你能负担得起它的依赖性占用时，使用singletons，否则使用GHC.TypeLits。singletons的优点是SingI型类便于进行基于归纳的分析，同时还依赖于GHC的特殊Nat型。
1正如评论中所指出的，并非每个Nat类居民都有KnownNat实例。例如，Any Nat :: Nat，其中Any是来自GHC.Exts的一个。只有居民0、1、2。。。具有CCD_ 41实例。