Свяжите необязательное натуральное число уровня типа (Возможно, Nat) со значением

Question

Функция natVal :: forall n proxy. KnownNat n => proxy n -> Integer связывает естественный уровень типа со значением 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 со значением? например, a 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)

Answer 2

То же, что мы всегда используем для преобразования типов в значения: классы типов.

class MaybeNatVal (v :: Maybe Nat) where
  maybeNatVal :: Proxy v -> Maybe Integer
instance MaybeNatVal Nothing where
  maybeNatVal _ = Nothing
instance KnownNat n => MaybeNatVal (Just n) where
  maybeNatVal x = Just $ natVal $ unJust x
    where unJust :: Proxy (Just n) -> Proxy (n :: Nat)
          unJust _ = Proxy

Библиотека, предложенная в другом ответе, делает то же самое, за исключением того, что классом типов является polymorphi c, а экземпляры - генерируется шаблоном Haskell.