haskell - 我必须每次都施放 Nat-kinds 吗？

Question

我尝试模拟一台量子计算机。这是代表量子比特的数据类型:

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

import Control.Monad
import Data.Maybe
import Data.Proxy
import Data.Type.Equality
import GHC.TypeNats

import Data.Group.Cyclic

data QBits :: Nat -> * where
    N :: QBits 0
    C :: KnownNat n => Bool -> QBits n -> QBits (n+1)
    S :: KnownNat n => Cyclic 4 -> QBits n -> QBits n -> QBits (n+1)

N 表示零个量子位。

C，代表“经典”，为第一个量子位分配一个 bool 值，并指定其余部分。

S，代表“叠加”，表示第一个量子位处于叠加状态，并为第一个量子位在测量时落入的每种可能性指定其余部分。它还指定了相位差，它是 Cyclic 4 中的一个值，它是环 Z/4Z 并且具有 Num 实例。

对于 instance Eq (QBits n)，我有一个解决方法，这样我就不会弄乱 Nat:

(=?=) :: QBits m -> QBits n -> Bool
N =?= N = True
C b x =?= C c y = b == c && x =?= y
S p x y =?= S q u v = p == q && x =?= u && y =?= v
_ =?= _ = False

instance Eq (QBits n) where
    (==) = (=?=)

然后我实现了 swapGate，它交换前两个量子位:

castNat :: forall f m n. (KnownNat m, KnownNat n) => f m -> Maybe (f n)
castNat x = do
    refl <- sameNat (Proxy :: Proxy m) (Proxy :: Proxy n)
    return (castWith (apply Refl refl) x)

swapGate :: KnownNat n => QBits n -> QBits n
swapGate (C b (C c x)) = C c (C b x)
swapGate (C b (S p x y)) = S p (C b x) (C b y)
swapGate (S r (C False x) (C False y)) = let
    Just y' = castNat y
    in C False (S r x y')
swapGate (S r (C False x) (S q u v)) = let
    Just u' = castNat u
    in S (r+q) (S r x u') (C True v)
swapGate (S r (C True y) (C False u)) = S (-r) (C True u) (C False y)
swapGate (S r (C True y) (C True v)) = let
    Just v' = castNat v
    in C True (S r y v')
swapGate (S r (C True y) (S q u v)) = let
    Just v' = castNat v
    in S (-r) (C True u) (S (r+q) y v')
swapGate (S r (S p x y) (C False u)) = let
    Just u' = castNat u
    in S p (S r x u') (C False y)
swapGate (S r (S p x y) (C True v)) = let
    Just v' = castNat v
    in S p (C False x) (S (p-r) y v')
swapGate (S r (S p x y) (S q u v)) = let
    Just u' = castNat u
    Just v' = castNat v
    in S p (S r x u') (S (q-p+r) y v')
swapGate z = z

我必须施放 Nat 的事实太烦人了。 castNat 真的是强制性的吗？

Answer 1

一方面，要解决语法上的问题，您可以这样写:

c :: forall f m n. (KnownNat m, KnownNat n) => f m -> f n
c = fromJust . castNat

然后:

swapGate :: KnownNat n => QBits n -> QBits n
swapGate (C b (C c x)) = C c (C b x)
swapGate (C b (S p x y)) = S p (C b x) (C b y)
swapGate (S r (C False x) (C False y)) = C False (S r x (c y))
swapGate (S r (C False x) (S q u v)) = S (r+q) (S r x (c u)) (C True v)
... etc. ...

正如评论中所解释的，潜在的“问题”是 GHC 对类型级自然数的内置推理非常有限。运算符将处理具体类型并处理一些特殊的抽象情况，例如 0 + m ~ m，但 GHC 无法进行其他甚至非常简单的推理，例如 m + 1 - 1 ~ m 或“m + 1 ~ n + 1 表示 m ~ n”。

您的选择是使用代数 Nat 类型(例如 Peano naturals)或使用求解器插件重写。

对于这个问题，Peano naturals 是一个(呃……)自然的选择，因为你对类型级自然值的所有操作都涉及增加或减少它们。将 Nat 和 + 类型运算符替换为:

data Nat = ZZ | SS Nat
type family m + n where
  ZZ + n = n
  SS m + n = m + SS n

并调整QBits定义:

data QBits :: Nat -> * where
    N :: QBits ZZ
    C :: Bool -> QBits n -> QBits (SS n)
    S :: Cyclic4 -> QBits n -> QBits n -> QBits (SS n)

无城堡定义的类型检查很好:

swapGate :: QBits n -> QBits n
swapGate (C b (C c x)) = C c (C b x)
swapGate (C b (S p x y)) = S p (C b x) (C b y)
swapGate (S r (C False x) (C False y)) = C False (S r x y)
swapGate (S r (C False x) (S q u v)) = S (r+q) (S r x u) (C True v)
swapGate (S r (C True y) (C False u)) = S (-r) (C True u) (C False y)
swapGate (S r (C True y) (C True v)) = C True (S r y v)
swapGate (S r (C True y) (S q u v)) = S (-r) (C True u) (S (r+q) y v)
swapGate (S r (S p x y) (C False u)) = S p (S r x u) (C False y)
swapGate (S r (S p x y) (C True v)) = S p (C False x) (S (p-r) y v)
swapGate (S r (S p x y) (S q u v)) = S p (S r x u) (S (q-p+r) y v)
swapGate z = z

或者，您可以使用求解器插件。安装 ghc-typelits-natnormalise 并添加:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

在你的代码的顶部，我可以去掉所有的强制转换，而且——再次——它的类型检查很好。

顺便说一下，这些解决方案中的任一个还允许您从代码中删除 KnownNat 约束。如果性能是一个考虑因素，那可能是一个胜利，因为您不必随身携带所有这些词典。