2

在 Haskell 中玩弄DataKinds，我生成了以下代码，它实现并滥用了一些类型级别的一元 nat：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Demo where
import Data.Proxy
import Data.Semigroup
import Numeric.Natural
import Data.Constraint

data Nat = Zero | Succ Nat

type family Pred (n :: Nat) where Pred ('Succ n) = n

class IsNat (n :: Nat) where
  nat :: proxy n -> Natural
  unNat :: proxy n -> (n ~ 'Zero => x) -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x) -> x

instance IsNat 'Zero where
  nat _ = 0
  unNat _ z _ = z

instance IsNat n => IsNat ('Succ n) where
  nat _ = succ (nat (Proxy @n))
  unNat _ _ s = s

noneIsNotSuccd :: (n ~ 'Zero, n ~ 'Succ (Pred n)) => proxy n -> a
noneIsNotSuccd _ = error "GHC proved ('Zero ~ 'Succ (Pred 'Zero))!"  -- don't worry, this won't happen

predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

data Indexed (n :: Nat) where
  Z :: Indexed 'Zero
  S :: Indexed n -> Indexed ('Succ n)

instance Show (Indexed n) where
  show Z = "0"
  show (S n) = "S" <> show n

recr :: forall n x. (IsNat n, Semigroup x) => (forall k. IsNat k => Indexed k -> x) -> Indexed n -> x
recr f Z = f Z
recr f (S predn) = predSuccIsNat (Proxy @n) (f predn) <> f (S predn)

main :: IO ()
main = print $ getSum $ recr (Sum . nat) (S Z)

当我尝试在 GHC 8.2.2 中编译它时，我收到以下类型错误：

Demo.hs:35:25: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: forall (n :: Nat) (proxy :: Nat -> *) r.
                                    n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:34:1-96
    • In the expression: unNat proxy (noneIsNotSuccd proxy) r
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |
35 | predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

这无疑是对 GHC 8.0.1 中发生的情况的改进，在 GHC 8.0.1 中它编译得很好，然后在运行时失败：

*** Exception: Demo.hs:34:23: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:33:1-78
    • In the expression: unNat proxy (noneIsNotSuccd proxy)
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy = unNat proxy (noneIsNotSuccd proxy)
(deferred type error)

似乎在 GHC 8.2.2 中，unNat采用了一个(IsNat (Pred n))未出现在类型签名中的隐式约束：

λ» :t unNat
unNat
  :: IsNat n =>
     proxy n
     -> (n ~ 'Zero => x)
     -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x)
     -> x

我有什么办法可以打电话unNat来实现类似的东西predSuccIsNat吗？

4

1 回答 1

3 
predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
                        ^^^^^

我不知道您希望从哪里获得IsNat您需要使用的字典unNat。如果我将它添加到类型签名

predSuccIsNat :: forall n proxy r. IsNat n => (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

一切正常（在 ghc 8.2.1 上，与 8.0.1 具有相同的延迟问题）。

没有它，您似乎想推断 if n ~ 'Succ (Pred n)then - 大概是从仅在 s 上定义IsNat n的事实。但即使能做出这样的推论，也还不够。例如，也不足以推断，您还需要.Pred nSuccn ~ Succ mIsNatIsNat m

于 2018-01-12T01:03:14.590 回答