类型构造器currying？（试图创建一个接受一个类型的数据构造函数，而创建另一个接受两种类型的数据构造函数）

Question

我刚刚开始学习Haskell，并且尝试通过制作纸牌游戏将其付诸实践。我正在尝试创建一个“手”类型，该类型表示固定大小的纸牌矢量（使用大小矢量，如下所述：https : //www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great -安全性/ haskell中的依存类型）

我对此进行了几次尝试，但是都没有成功：

{-# LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

import Data.Type.Natural
import Data.Vector.Sized (Vector)
import Card -- | I have the Card type defined in another file

data Hand (n :: Nat) where
    Hand :: SNat n -> Vector Card n

{- fails with:
* Data constructor 'Hand' returns type 'Vector Card n'
    instead of an instance of its parent type 'Hand n'
* In the definition of data constructor 'Hand'
  In the data type declaration for 'Hand'
-}

type Hand = Vector Card

{- compiles, but it doesn't work as expected:
ghci> :k Hand
Hand :: *
(whereas I'd expect 'Hand :: Nat -> Vector Card Nat' or something)
-}

我不太确定该怎么称呼，好像是类型构造函数引起了我的注意，但也许我完全错了。我一直无法在网上找到类似的内容。在此先感谢您的帮助！

Answer 1

Vectorfrom Data.Vector.Sized会将大小作为第一个参数，而不是第二个，与链接教程中的不同。所以你需要

type Hand n = Vector n Card

至于您的GADT变体，您只是缺少构造函数的结果类型。

data Hand (n :: Nat) where
    Hand :: SNat n -> Vector n Card -> Hand n
                                   ^^^^^^^^^^

GADT构造函数类型始终需要它们定义的任何类型的共域。就是说，我认为SNat这里是没有必要的-如果手中有多少张牌的信息来自外部，则也没有理由将其保留在内部。