我刚刚开始学习Haskell,而我正试图通过制作纸牌游戏来实践它。我正在尝试创建一个类型“手”,它代表一个固定大小的卡片矢量(使用这里描述的大小向量:https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-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)
-}
我不太确定该怎么称呼它,它看起来像是类型构造函数向我说,但也许我完全错了。我无法在网上找到类似的东西。在此先感谢您的帮助!
来自Vector
的Data.Vector.Sized
将大小作为第一个参数,而不是第二个参数,与链接教程不同。所以你需要
type Hand n = Vector n Card
至于你的GADT变体,你只是缺少构造函数的结果类型。
data Hand (n :: Nat) where
Hand :: SNat n -> Vector n Card -> Hand n
^^^^^^^^^^
GADT构造函数类型总是需要它们定义的任何类型的codomain。也就是说,我认为这里的SNat
是不必要的 - 如果手中有多少张牌的信息来自外部,那么也没有理由在内部抓住它。