类型构造函数currying? (尝试创建一个数据构造函数,从另一个接受两种类型的数据构造函数接受一种类型)

问题描述 投票:3回答:1

我刚刚开始学习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)
-}

我不太确定该怎么称呼它,它看起来像是类型构造函数向我说,但也许我完全错了。我无法在网上找到类似的东西。在此先感谢您的帮助!

haskell types currying dependent-type type-constructor
1个回答
5
投票

来自VectorData.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是不必要的 - 如果手中有多少张牌的信息来自外部,那么也没有理由在内部抓住它。

© www.soinside.com 2019 - 2024. All rights reserved.