Associate a type level optional natural number (Maybe Nat) with a value

user_2072459 0
Viewed 195

The function natVal :: forall n proxy. KnownNat n => proxy n -> Integer associates a type level natural with an Integer value. Using DataKinds, TypeApplications language extensions one can do

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

module Derp where

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

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

How would one associate a 'Maybe Nat to a value? e.g. a Maybe Integer

foo2 :: Maybe Integer
foo2 = maybeNatVal (Proxy @(Just 1337))
type-level-computation haskell
2 Answers

This is what the singletons package does. The relevant function is named demote. demote, specialized with a type-level value (with a visible type application), is equal to the corresponding term-level value.

One difference to mention is that Nat demotes to Natural.

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

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

The same thing we always use to convert types to values: typeclasses.

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

The library suggested in the other answer does the same thing, except the typeclass is polymorphic and the instances are generated by Template Haskell.

user_56842570
Related