haskell - 将 Nat 从类型族调用转换为 Integer

Question

import Data.Singletons
import Data.Singletons.TypeLits

type family N t :: Nat where
  N Int = 42
  N String = 9

foo :: (n ~ N t) => t -> Integer
foo _ = fromSing (sing :: Sing n)

失败

• Could not deduce: DemoteRep * ~ Integer
  from the context: n ~ N t
    bound by the type signature for:
               foo :: n ~ N t => t -> Integer
    at mini.hs:16:1-32
• In the expression: fromSing (sing :: Sing n)
  In an equation for ‘foo’: foo _ = fromSing (sing :: Sing n)

如何修复它？

Answer 1

您的代码有两个问题。首先，(sing::Sing n) 范围内没有 n。您需要显式 forall 才能将其纳入范围。

其次，如果你想要SingI，你需要这么说。 GHC 不知道也不会检查所有 t 的 N t 是否为 SingI，顺便说一句，这实际上不是真的: N Bool 具有 Nat 类型，但没有 SingI (N Bool)。

因此，解决方案:

foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing :: Sing (N t))

或者使用类型应用程序:

foo :: forall t. SingI (N t) => t -> Integer
foo _ = fromSing (sing @_ @(N t))