结合`SomeNat`和`Nat`

我下面的例子中列明的问题Can I have an unknown KnownNat?结合`SomeNat`和`Nat`

我想作一个小改动的代码。

原始代码是

{-# 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 [email protected](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 [email protected](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 nKnownNat (n + 5)？

来源

2015-09-01 Alpaca

我的猜测是GHC无法将n + 5减少为任何类型的正常形式，并且因为它不能查找类型实例 - 因为它不知道它在找什么！在不知道n是什么的情况下，对n + 5的评价无法进行（假设通过左边的论证进行归纳定义的典型问题）。我不太了解KnownNat如何工作背后的魔力，但它可能只知道如何找到该实例，如果它给了一个具体的类型。 – ocharles

如果知道'n'，GHC就不知道'n + 5'是已知的。已知的唯一'Nat'表达式是数字文字。另一方面，如果您在类型级别上使用自定义一元数字，并且以归纳方式实现已知性和附加性，则可能会导致更多的事实对GHC显而易见，包括所涉及的含义。 –

如果已知的唯一'Nat'表达式是数字文字，那么第一个示例如何工作？ – Alpaca

第一个例子是纯粹的神奇someNatVal，它制造了一个类型级别Nat和知识去与它。在第二个例子中，你有n的知识，但你在问关于n+5。有两个原因不起作用。

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

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

由于这些问题，似乎对于许多目的而言，必须抛开轻松有效的机制来支持The Slow Way，手工构建一元自然数，可在singleton-nats中找到。您需要单独的函数来处理值和类型级别的计算，但至少类型检查器会确保它们匹配正确，并且有一些模板Haskell可以尝试使其一次写入更容易。

来源

2015-09-27 05:49:07 dfeuer

结合`SomeNat`和`Nat`

回答

相关问题