将类型级别的可选自然数（Maybe 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)

如何将 a'Maybe Nat与一个值相关联？例如一个Maybe Integer

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)