haskell - 结合 `SomeNat` 和 `Nat`

我正在按照问题 Can I have an unknown KnownNat? 中列出的示例进行操作

我想对代码做一个小改动。

原来的代码是

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar n
                a = Bar "as"
            print $ bar a

它按预期工作。我想进行更改，修改类型级别 n 。

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar (n + 5)
                a = Bar "as"
            print $ bar a

我得到的错误信息是

    Could not deduce (KnownNat (n + 5)) arising from a use of ‘bar’
    from the context (KnownNat n)
      bound by a pattern with constructor
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,
               in a case alternative
      at Blag.hs:19:9-30
    In the second argument of ‘($)’, namely ‘bar a’
    In a stmt of a 'do' block: print $ bar a
    In the expression:
      do { let a :: Bar (n + 5)
               a = Bar "as";
           print $ bar a }
Failed, modules loaded: none.

为什么编译器不能从 KnownNat (n + 5) 推导出 KnownNat n ？

最佳答案

第一个示例通过 someNatVal 的纯粹魔法起作用，它生成类型级 Nat 和与之配套的知识。在第二个示例中，您了解 n ，但您询问的是 n+5 。这行不通有两个原因。

第一个问题是类型系统会将所有“额外”实例视为不连贯的。也就是说，它需要知道 KnownNat 2 和 KnownNat 7 以及 KnownNat n => KnownNat (n + 5) 和 KnownNat n => KnownNat (5 + n) 等等。这些实例都会相互冲突，因此编译器需要有关如何处理这种情况的特殊内置知识，一切都会相当痛苦。

另一个问题是 TypeLits 非常简单。它们似乎没有您期望从类型级自然中获得的有用归纳结构。

由于这些问题，似乎出于许多目的，必须放弃简单高效的 TypeLit 机制，转而支持 The Slow Way，您可以在 singleton-nats 中找到手工构建的一元自然数。您需要单独的函数来处理值和类型级别的计算，但至少类型检查器将确保它们正确匹配，并且有一些 Template Haskell 将尝试使同时编写更容易。

关于haskell - 结合 `SomeNat` 和 `Nat`，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/32331537/