haskell - 将类型级别的可选自然数(可能是 Nat)与值相关联

Question

函数natVal :: forall n proxy. KnownNat n => proxy n -> Integer将类型级别 natural 与 Integer 值相关联。使用 DataKinds、TypeApplications 可以做的语言扩展

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}

module Derp where

import           Data.Proxy                     ( Proxy(..) )
import           GHC.TypeLits                   ( natVal )

foo :: Integer
foo = natVal (Proxy @1337)

如何将 'Maybe Nat 与一个值相关联？例如一个 可能是整数

foo2 :: Maybe Integer
foo2 = maybeNatVal (Proxy @(Just 1337))

Answer 1

这就是 singletons 包的作用。相关函数名为 demote。 demote，专用于类型级值(具有可见类型应用程序)，等于相应的术语级值。

要提到的一个区别是 Nat 降级为 Natural。

{-# LANGUAGE TypeApplications, DataKinds #-}
import Data.Singletons
import Numeric.Natural (Natural)  -- base

myexample :: Maybe Natural
myexample = demote @('Just 1337)