8

是否可以在 Haskell 中为部分应用类型创建数据构造函数？

ghci 会话：

Prelude> data Vector a b = Vector {x::a, y::b}
Prelude> :t Vector
Vector :: a -> b -> Vector a b
Prelude> type T1 = Vector Int
Prelude> :t T1
<interactive>:1:1: Not in scope: data constructor `T1'
Prelude> let x = Vector
Prelude> let y = T1
<interactive>:46:9: Not in scope: data constructor `T1'

我想为 T1 类型创建数据构造函数-甚至可能吗？还是我必须使用新类型，因为无法手动定义这样的功能？

4

4 回答 4

6

我对你的目标有点困惑，但让我们一点一点地来看看，也许我会找到正确的观点：

:t告诉你变量的类型；应用于类型时没有任何意义，因为它只会返回您传递的内容。请注意这里的错误告诉您:t需要某种数据值作为参数：

Prelude> :t Maybe

<interactive>:1:1: Not in scope: data constructor `Maybe'
Prelude> :t (Maybe Integer)

<interactive>:1:2: Not in scope: data constructor `Maybe'

<interactive>:1:8: Not in scope: data constructor `Integer'

您可以创建部分类型：

Prelude> type T = Maybe
Prelude> Just 5 :: T Integer
Just 5

type T a = Maybe a -- alternately, with explicit type parameters
Prelude> Just 'a' :: T Char
Just 'a'

您不能为部分类型创建数据构造函数，因为它们不代表数据。Maybe没有在类型上参数化的情况下，a 可以或具有哪些值Vector？您可能倾向于认为Maybe可能具有 value Nothing，但Nothing键入为：

Prelude> :t Nothing
Nothing :: Maybe a

关键是 thatNothing可以是any Maybe a，但它仍然需要a知道它是Nothing. （这有点像我告诉你“给我拿一杯”而不是“给我拿一杯任何东西”——在我至少完成我的想法之前，你不能有效地遵守）。

您当然可以创建部分应用的函数，一旦应用它们就会返回一个完整的类型：

Prelude> let f = Just :: a -> T a
Prelude> f 5
Just 5
Prelude> :t f 'a'
f 'a' :: T Char
于 2013-07-23T20:07:09.500 回答
4

GADT 可以做到这一点。GHCi 会话：

λ :set -XGADTs
λ :{
| data Vector a b where
|     Vector :: a -> b -> Vector a b
|     T1 :: Int -> b -> T1 b
| type T1 = Vector Int
| :}
λ :t T1
T1 :: Int -> b -> T1 b
于 2013-07-23T19:03:49.920 回答
1

已经有一个构造函数T1，它被命名为Vector：

*Main> :t Vector :: Int -> b -> T1 b
Vector :: Int -> b -> T1 b :: Int -> b -> T1 b
于 2013-07-24T03:38:59.567 回答
1 
Prelude> type T1 = Vector Int

This creates a type constructor for a Vector Int. Note that here Vector is used as a type constructor because you supply a type argument. You can query the kind of the type T1 with :k:

Prelude> :k T1
T1 :: * -> *

This tells you that T1 is a type constructor that takes a concrete type (*) and returns a concrete type.

To create a data constructor, you need to provide a data value for the first parameter of the Vector data constructor:

Prelude> let t1 = Vector 5
Prelude> :t t1
t1 :: b -> Vector Integer b

(Note that Vector is both a type* constructor as well as a data constructor because you used the same name on the left and right sides of the data declaration.)

于 2013-07-24T19:15:43.513 回答