haskell - TypeLits 或 Singletons : Promoting an `Integer` to `KnownNat` (`Nat` ) at Runtime

Question

我发现了两种在运行时将 Integer 提升为 Nat(或 KnownNat，我还没有得到区分)的方法，使用 TypeLits 和 Proxy(Data.Proxy 和 GHC.TypeLits)，或 Singletons(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 的文档表示它不应该被开发人员使用，但是 Singletons 不会捕获给定 Integer 不是自然数的情况(即，运行 playingWithTypes 8 运行没有错误，但 playingWithTypes (-2) 在我们尝试创建时失败来自非自然数的单例)。

那么，推广 Integer 的“标准”方式是什么？到 Nat ?或者使用 TypeLits 和 Proxy 或 Singleton 进行推广的最佳方法是什么？

Answer 1

Nat (or KnownNat, I don't get the distintion yet)

Nat是类型级别的自然数。它没有学期级别的居民。这个想法是 GHC 将任何自然数提升到类型级别，并赋予它类型 Nat .
KnownNat是一种约束，在某种东西上 Nat ，其实现见证了如何转换实物 Nat到术语级别 Integer . GHC 自动创建 KnownNat 的实例适用于所有类型级别的居民 Nat 1.

也就是说，即使每个 n :: Nat (读取类型 n 的种类 Nat )具有 KnownNat在 it1 上的实例，您仍然需要写出约束。

I've found two ways to promote an Integer to a Nat

你真的有吗？在一天结束时， Nat在今天的 GHC 中简直是神奇的。 singletons发挥同样的魔力。在引擎盖下，它 uses someNatVal .

So, what is the "standard" way to promote an Integer to a Nat? Or what is the best approach to promote, using GHC.TypeLits and Proxy, or singletons?

没有标准的方法。我的看法是:使用 singletons当你负担得起它的依赖足迹和 GHC.TypeLits否则。 singletons的优势|是 SingI type 类可以方便地进行基于归纳的分析，同时仍然依赖于 GHC 的特殊 Nat类型。

1 正如评论中所指出的，并非 Nat 的每个居民实物有 KnownNat实例。例如， Any Nat :: Nat在哪里 Any是 one from GHC.Exts .只有居民 0 , 1 , 2 , ... 有 KnownNat实例。