TypeLits或Singletons:在运行时将`Integer`提升为`KnownNat`(`Nat`)

Question

我发现有两种方法可以在运行时使用TypeLits和Proxy(Data.Proxy和GHC.TypeLits)或Singletons(Data.Singletons)在运行时将Integer提升为Nat(或KnownNat,我还没有得到区别). ).在下面的代码中,您可以看到如何使用这两种方法中的每一种:

{-# 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)当我们尝试创建Singleton时失败)来自非自然数).

那么,推广一个"标准"的方式Integer是Nat什么？或者使用TypeLits和Proxy或Singletons进行推广的最佳方法是什么？

Answer 1

Nat(或者KnownNat,我还没有得到区分)

Nat是那种类型级自然数.它没有任期级别的居民.这个想法是GHC将任何自然数字提升到类型级别,并给予它类型Nat.

KnownNat在某种形式上是一种约束,Nat其实现见证了如何将类型的东西转换Nat为术语级别Integer.GHC自动KnownNat为所有类型级别的居民创建实例Nat¹.

这就是说,即使每一个n :: Nat(读式n那种Nat)有一个KnownNat在它的实例¹,你仍然需要写出来的约束.

我找到了两种促进Integera的方法Nat

你真的吗？在一天结束时,Nat在今天的GHC简直是神奇的.singletons利用同样的魔力.在引擎盖下,它使用someNatVal.

那么,推广一个"标准"的方式Integer是Nat什么？或者,推广,使用GHC.TypeLits和Proxy/或单身的最佳方法是什么？

没有标准的方法.我的看法是:singletons当你能负担得起它的依赖足迹时使用GHC.TypeLits.优点singletons是SingI类型类可以方便地进行基于归纳的分析,同时还依赖于GHC的特殊Nat类型.

¹正如评论中所指出的,并非每个居民Nat都有一个KnownNat例子.例如,Any Nat :: Nat其中Any是从一个GHC.Exts.只有居民0,1,2,...有KnownNat实例.