тип конструктора карри? (пытаясь создать конструктор данных, принимающий один тип от другого конструктора данных, принимающий два типа) - PullRequest
Новая
       32

тип конструктора карри? (пытаясь создать конструктор данных, принимающий один тип от другого конструктора данных, принимающий два типа)

3 голосов
/ 21 марта 2019

Я только начинаю изучать 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)
-}

Я не совсем уверен, как это назвать, мне кажется что-то вроде конструктора типов, но, возможно, я совершенно не прав. Я не смог найти что-то подобное в Интернете. Заранее спасибо за помощь!

1 Ответ

5 голосов
/ 21 марта 2019

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 всегда нужен кодомен любого типа, который они определяют. Тем не менее, я думаю, что SNat здесь не нужно - если информация о том, сколько карт находится в руке, приходит извне, нет никакой причины удерживать ее и внутри.

...