Haskell类型的功能？

Question

考虑这个ADT:

data Property f a = Property String (f a) | Zilch
  deriving Show

这是什么f？它是一个功能a吗？它是'类型函数'吗？教练说Haskell有一个图灵完整类型的语言......所以在这种情况下,类型也可以具有函数我假设？

*Main> var = Property "Colors" [1,2,3,4]
*Main> :t var
var :: Num a => Property [] a

怎么f样[]在这里？既然[]是空列表的构造函数,那么它f总是将成为a以下示例中类型的最外面的空构造函数？

*Main> var = Property "Colors" [(1,"Red"),(2,"Blue")]
*Main> :t var
var :: Num t => Property [] (t, [Char])

*Main> var = Property "Colors" (1,"Red")
*Main> :t var
var :: Num t => Property ((,) t) [Char]

后者我不太明白,但如果有人说Haskell推断出那个元组的空构造函数,我可以买到它.另一方面,

*Main> var = Property "Colors" 20
*Main> :t var
var :: Num (f a) => Property f a

什么在f这里？不能是身份,因为id :: a -> a我们需要(f a).

我设法让我的ADT成为一个仿函数:

instance Functor f => Functor (Property f) where
  fmap fun (Property name a) = Property name (fmap fun a)
  fmap g Zilch               = Zilch 

所以类似下面的工作

*Main> var = Property "Colors" [1,2,3,4]
*Main> fmap (+1) var
Property "Colors" [2,3,4,5]

但是,如果我把它放到前面的元组示例中呢？

我真的在寻找解释性答案(在夏季课程中已经看过Haskell仅仅两个月),而不是提到FlexibleContexts允许...说fmap任意工作的事情a.

Answer 1

你已经对(令人困惑的)事实感到困惑,这个事实[]意味着在Haskell的不同背景下有两个不同的事情,这使你很难解释其余的实验.

在值级别[]确实是列表的空构造函数.但是当你询问类型时Property "Colors" [1,2,3,4],看到Property [] a你正在查看类型表达式,而不是值表达式.类型级别没有空列表.¹而是列表类型[]的类型构造函数.你可以拥有[Int](整数列表的类型),[Bool](bool列表的类型),或[a](列表的多态类型a); []是真实被应用到的东西Int,Bool以及a在这些例子.

你实际上可以[Int]像[] Int你想要的那样写,虽然它看起来很奇怪,所以你通常只[]在类型级别看到你想要使用它时未应用.

让我们再看看你的数据声明:

data Property f a = Property String (f a) | Zilch

在左侧,您已经声明了该类型 的形状Property; Property f a形成一种类型.在右侧,通过列出可能的值构造函数(和)以及这些构造函数中"槽"的类型(无一个类型;一个类型的槽和另一个类型)来声明该类型中的值的形状.类型,为).PropertyZilchZilchStringf aProperty

因此,我们可以告诉无论什么f和a类型,类型表达式f a(f应用于a)必须形成具有值的类型.但f并不一定(实际上它不可能)是一种正常的价值观!没有类型的时隙f中的Property值的构造器.

一个更清晰的例子就是这样:

*Main> var = Property "Stuff" (Just True)
*Main> :t var
var :: Property Maybe Bool

如果你不知道它,Maybe是一个内置类型,其声明如下所示:

data Maybe a = Just a | Nothing

这个例子很好,因为我们没有在类型级别和值级别使用相同的名称,这可以避免在您尝试了解事物的运作方式时出现的混淆.

Just True是类型的值Maybe Bool.在值级别,我们将Just数据构造函数应用于值True.在类型级别,我们将Maybe 类型构造函数应用于该类型Bool.Maybe Bool值进入值构造函数的f a槽中Property,它恰好适合:fis Maybe和ais Bool.

所以回到原来的例子:

*Main> var = Property "Colors" [1,2,3,4]
*Main> :t var
var :: Num a => Property [] a

你正在填补f a空缺[1, 2, 3, 4].这是一个某种数字的列表,所以它会Num t => [t].所以ain f a是t(有一个Num需要出现的约束),并且f是列表类型构造函数 [].这[]就像Maybe,不喜欢Nothing.

*Main> var = Property "Colors" (1,"Red")
*Main> :t var
var :: Num t => Property ((,) t) [Char]

这里的f a插槽正在填充(1, "Red"),这是一种类型Num t => (t, [Char])(记住这String只是另一种写作方式[Char]).现在要了解这一点,我们必须有点挑剔.忘记现在的约束,只关注(t, [Char]).不知何故,我们需要将其解释为应用于其他内容的东西,因此我们可以将其与之匹配f a.事实证明,虽然我们有元组类型的特殊语法(比如(a, b)),但它们就像普通的ADT一样,你可以在没有特殊语法的情况下声明.A 2元组类型是类型构造函数,我们可以写(,)应用于其它两种类型,在这种情况下t和[Char].我们可以使用部分应用的类型构造函数,因此我们可以将(,)应用t视为一个单元,并将该单元应用于[Char].我们可以将这种解释写成Haskell类型的表达式((,) t) [Char],但我不确定它是否更清楚.但是它归结为是,我们可以匹配这f a被征服的"单位" (,) t作为f和[Char]作为a.然后它给了我们Property ((,) t) [Char](只有我们也必须放回Num t我们之前忘记的约束).

最后这一个:

*Main> var = Property "Colors" 20
*Main> :t var
var :: Num (f a) => Property f a

在这里,我们f a用20一些数字填充插槽.我们还没有准确指出数字的类型,所以Haskell愿意相信它可以是类中的任何类型Num.但是我们仍然需要类型具有我们可以匹配的"形状" f a:某些类型构造函数应用于其他类型.它是整个类型表达f a需要相匹配的类型20,所以这是什么有一个Num约束.但是我们还没有说过什么f或者a可能是什么,并且20可以通过满足约束的任何类型Num,因此它可以是Num (f a) => f a我们想要的任何类型,因此为什么你的类型var仍然是多态的(f并且a只是添加了约束).

你可能只看到数字类型,如Integer,Int,Double,等,所以不知道如何有可能可能是一个f a这是一个数; 所有这些例子都只是单一的基本类型,而不是应用于某些东西.但是你可以编写自己的Num实例,所以Haskell从不假设给定的类型(或类型的形状)不能是一个数字,如果你真的试图使用它并且它找不到Num实例,它就会抱怨.所以有时你会得到这样的东西,这可能是错误,但是Haskell接受(现在)一个Num你不期待的奇怪事物的类型.

事实上,内置库中已有类型具有复合类型级结构并具有Num实例.一个例子是Ratio用于将分数表示为两个整数的比率的类型.你可以拥有一个Ratio Int或一个Ratio Integer,例如:

Main*> 4 :: Ratio Int
4 % 1

所以你可以说:

*Main> var = Property "Colors" (20 :: Ratio Integer)
*Main> :t var
var :: Property Ratio Integer

¹实际上可以DataKinds启用扩展,允许类型镜像几乎任何值的结构,因此您可以拥有类型级列表.但这不是正在发生的事情,它并不是一个你可以使用的功能,直到你已经很好地处理类型和值在vanilla Haskell中工作的方式,所以我建议你忽略这个脚注并假装它还不存在.

Answer 2

这是什么f？它是一个功能a吗？它是'类型函数'吗？

是的,它确实是一个类型函数,在某种意义上它接受一个类型并产生一个类型,即它的类型是Type -> Type- 或者,正如Haskell传统上写的那样

> :k []
[] :: * -> *

怎么f样[]在这里？既然[]是空列表的构造函数...

这是一个误解.实际上[]在Haskell中有两个不同的东西:

2. 列表值构造函数 [] :: [a].这会生成一个空列表(或任意包含类型 - 因为它实际上包含零元素,无论如何您不关心该类型).

和

1. 列表类型构造函数 [] :: * -> *.这需要一个类型,并给出包含该类型值的列表的类型.这个论点很重要,因为大多数有趣的列表显然不是空的.

在Property [] a,你正在处理类型构造函数,与值构造函数不同,它是一个对类型进行操作的函数,因此你可以实例化它f.

Property ((,) t) [Char]

在这里,您发现了另一个类型级函数:元组类型构造函数.这需要两个类型参数并给出一个类型(这些类型的元组).有了(,) t你已经把它应用到一个类型参数,但保留其他开放的,所以你可以再次使用它作为像一个参数的类型的功能f.