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 回答