数据族实例: newtype、data

Question

对于Haskell 98 decls，整个数据类型必须是newtype或data。但数据系列可以混合使用newtype instance、data instance。这是否意味着newtype是数据构造函数的属性，而不是数据类型的属性？有没有可能有Haskell这样的东西：

data Foo a = MkFoo1 Int a
           | MkFoo2 Bool a
           | newtype MkFoo3 a

我知道我不能写下面的内容，但是为什么/哪里出错了？：

data family Bar a

newtype instance Bar (Maybe Int)  = MkBar1 (Maybe Int)
            -- MkBar1 :: (Maybe Int) -> Bar (Maybe Int), see below

newtype instance Bar [Char]  = MkBar2 [Char]

data instance Bar [Bool]  where
  MkBar3 :: Int -> Bool -> Bar [Bool]
  -- can't be a newtype because of the existential Int

-- we're OK up to here mixing newtypes and data/GADT

data instance Bar [a]  where
  MkBar4 :: Num a => a -> Bar [a]
  -- can't be a newtype because of the Num a =>

我不能这样写，因为实例头Bar [a]与MkBar2, MkBar3的两个头重叠。然后，我可以通过在Bar [a]的where ...中移动这两个构造函数decls来解决这个问题。但是MkBar2会变成一个GADT (因为它的结果类型不是Bar [a])，所以不能是newtype。

那么，作为newtype是结果类型的属性，而不是构造函数的属性吗？但是考虑一下上面为newtype实例MkBar1推断的类型。我不能编写具有相同类型的顶级newtype

newtype Baz a  where
  MkBaz :: (Maybe Int) -> Baz (Maybe Int)

-- Error: A newtype constructor must have a return type of form T a1 ... an

嗯？MkBar1是一个新类型的构造函数，它的类型不是这种形式。

如果可能，请在不深入讨论角色的情况下进行解释:我试图理解它们；这只会让我头疼。从构造和模式匹配的角度来讨论这些构造函数。

Answer 1

您可以将数据族视为(注入和开放)类型族的更强版本。正如您从this question I asked a while back中看到的，数据系列几乎可以用内射类型系列来伪造。

这是否意味着成为新类型是数据构造函数的属性，而不是数据类型？有没有可能有Haskell这样的东西：

data Foo a= MkFoo1 Int a| MkFoo2 Bool a|新类型MkFoo3 a

不是的。作为newtype绝对是类型构造函数的属性，而不是数据构造函数的属性。数据族，与类型族非常相似，有两个级别的类型构造函数：

实例data/type instance FamInstTyCon a = ...的类型构造函数data/type family FamTyCon a

• the类型构造函数的

同一个data/type系列构造函数的不同实例仍然是根本不同的类型-它们恰好统一在一个类型构造函数下(该类型构造函数将是内射的和生成性的-有关这一点的更多信息，请参阅链接问题)。

通过类型族的类比，您不会期望能够在TyFam a类型的东西上进行模式匹配，对吧？因为您可能有type instance TyFam Int = Bool和type instance TyFam () = Int，并且您无法静态地知道您正在查看的是Bool还是Int！

Answer 2

这些是等效的：

newtype          NT a b  = MkNT (Int, b)

data family DF a b
newtype instance DF a b  = MkDF (Int, b)

-- inferred MkNT :: (Int, b) -> NT a b
--          MkDF :: (Int, b) -> DF a b

此外，您不能在系列DF中声明任何其他实例/构造函数，因为它们的实例头部会与DF a b重叠。

Q re standalone newtype Baz中的错误消息具有误导性

-- Error: A newtype constructor must have a return type of form T a1 ... an

(而且可能是在有数据家族之前的时间)。newtype构造函数必须具有与实例头完全相同的返回类型(如果使用GADT语法，则以alpha为模重命名)。对于独立的新类型，“实例头”指的是newtype头。

对于非newtype数据实例，各种构造函数可能具有比实例头更具体的返回类型(这使它们成为GADT)。

在data/newtype实例头中声明的类型(在文献中被不同地称为“Type scheme”，“monotype”--因为没有约束，在2008年的论文“type Checking with Open type Functions”中称为“Function-free type”)是所有构造函数的返回类型必须统一的主要类型。(可能没有任何构造函数恰好具有该返回类型。)

如果您的实例是一个newtype，则规则要严格得多:只能有一个构造函数，并且其返回类型必须恰好是主体类型。所以为了回答最初的问题

是否意味着newtype是数据构造函数的属性，而不是数据类型？但是..。那么，作为newtype是结果类型的属性，而不是构造函数的属性吗？

不，不是构造函数；是的，更像是结果:作为一个新类型是一个数据族实例/它的主体类型的属性。只是对于独立的newtype，实际上只能有一个实例，并且它的主体类型是该类型构造函数最通用的类型。从派生的角度来看，我们可以说newtype的主体类型/返回类型唯一地标识了一个数据构造函数。这对于类型安全至关重要，因为该类型的值与newtype的数据构造函数中的类型共享其表示形式，即没有包装器--正如@AlexisKing的注释所指出的那样。那么模式匹配就不需要去寻找构造函数:匹配是不可反驳的/构造函数是虚拟的。

我突然想到，为了更精确地输入类型/更好地编写文档，您可能希望将newtype声明为只有一个实例的数据族，其头部比必须放在独立newtype中的值更具体。