我試圖澄清一些 Haskell 概念，并想知道是否有人可以提供幫助。

通過資料宣告定義型別時，例如：

資料 DatumType ab = 基準 ab

我一直想知道型別是DatumType還是隱含 forall a. DatumType a b的。

因為確實有ExplicitForAll

λ> :set -XExplicitForAll
λ> :k forall a. Maybe a
forall a. Maybe a :: *

λ> :k forall a b . DatumType a b
forall a b . DatumType a b :: *

λ> :k DatumType
DatumType :: * -> * -> *

我們可以看到種類forall a b. DatumType a b是proper type i.e. *

然而 DatumType 本身只是一個型別建構式。

因此，這意味著諸如 [a] 之類的多型型別是 TYPE（即 *），并且該型別的全名是forall a. [a]

換句話說，我要確認的是，haskell 中的多型型別宣告始終采用縮寫形式，并且完整的型別名稱始終帶有隱式forall a. ....

也就是說， indata Mytype a型別不僅Mytype是Mytype a，而且forall a. Mytype a, whileMytype是型別建構式。

這種解釋正確嗎？

EDIT1（在@Daniel Wagner 回答之后）

我想我會編輯這個問題，以解釋所有澄清的東西來自哪里。假設在學習和試驗型別類時，我對實體 Eq (a,b) 感到困惑。為什么不實體化 Eq(,)，答案不僅僅是因為在實作中需要參考型別變數。Eq 只能在正確的型別上定義，任何可能的對實際上都是一種型別，一種多型型別。那么問題來了，但是當我們寫 data (,) ab = (,) ab 時，我們在定義什么。我是在定義 (,) 還是 forall a b。（一，乙）。

Edit2（按照@Ben 回答）

One of the material that drove my formalisation together with the :set -XExplicitForAll experiment above is the following statement taken from here A Gentle Introduction to Haskell, Version 98 - 2 Values, Types, and Other Goodies

Haskell also incorporates polymorphic types---types that are universally quantified in some way over all types. Polymorphic type expressions essentially describe families of types. For example, (forall a)[a] is the family of types consisting of, for every type a, the type of lists of a. Lists of integers (e.g. [1,2,3]), lists of characters (['a','b','c']), even lists of lists of integers, etc., are all members of this family.

uj5u.com熱心網友回復：

翻譯成英文的定義data DatumType a b = Datum a b是這樣的：

假設有一個名為的新型別建構式DatumType和一個名為的新資料建構式Datum，這樣對于所有型別aand b，Datum應用于 type 的值，a并且 type 的值產生 typeb的值DatumType a b。

我一直想知道型別是DatumType還是隱含 forall a. DatumType a b的。

我認為理解這里的障礙是術語“型別”可以有兩種不同的含義，具體取決于背景關系：

1. 型別是存在于型別級別的任何物體
2. 型別具體是那些可以作為術語型別的型別級物體；任何類似的東西Type（也稱為*），并且只有這樣的東西

這兩個定義的出現基本上是因為我們使用短語“type of”來描述術語級別的事物與型別級別的事物之間的關系——因此將不能參與該關系的事物包含在“型別”。然而，型別運算式中存在很多不能直接參與這種關系的東西，我們想談論它們，而不必一直使用像“型別級物體”這樣的笨拙短語。作為一個社區，我們似乎沒有想出比在不同時間在這兩種意義上使用“型別”更好的解決方案，并希望從背景關系中清楚。

所以很明顯這DatumType不是定義2的型別；它需要應用于兩個型別引數才能在術語級別產生某種型別。如果這就是我們的想法，那么我可以理解為什么您會傾向于認為資料宣告定義的“型別”是forall a b. DatumType a b.

但是，我認為這可能是一種令人困惑的思考方式。就其本身forall a b. DatumType a b而言，是可以在所有型別的表格中使用的術語型別DatumType _ _；這種型別的唯一值是Datum undefined undefined. 相反forall a b，當您看到時，通常會更遠DatumType a b；例如，Datum建構式本身的型別（如果您使用 GADT 語法定義它，您將撰寫它）可以寫為Datum :: forall a b. a -> b -> DatumType a b.

所以說“資料宣告定義的型別forall a b. DatumType a b很奇怪。資料宣告定義了一整套型別，其中型別forall a b. DatumType a b是一個極其有限（而且相當無用）的例子。相反，我會說“對于所有型別a和b，資料宣告定義了一個型別DatumType a b"；所涉及的"for all"概念的范圍比你forall在單個型別運算式中用關鍵字表達的范圍更廣，所以我把它從正式的型別運算式中移到了英文描述中。

當然，如果我們專注于“型別”的定義 1，那么事情就更容易解釋了。資料宣告只是DatumType用 kind定義了一個型別* -> * -> *。

這就引出了一個問題：哪種觀點是正確的？

也許令人不滿意的是，這兩種觀點之間沒有什么有趣的事情發生。這兩件事都發生了：我們得到了一個新的型別建構式DatumType，它有 kind * -> * -> *，并且對于所有型別a，并且b DatumType a b是某些術語的型別。這就是善意的* -> * -> * 意思。只有當您嘗試識別“型別”而沒有意識到術語型別在這兩種意義上都經常使用時，才會出現困境，所以如果您不清楚自己在使用哪種意義上，您可能會犯錯。

Some contexts say that things which don't have kind * are not types, and therefore DatumType is not really a type. Others talk about DatumType as a type. However that is purely a difference in what terminology we choose to use; either way DatumType :: * -> * -> * is a thing that exists, and it functions the same in either viewpoint. Getting hung up on whether a particular type-level entity is or is not a type is not a question of how things really work, it's just a question of English language usage.

So to come back to some of your more specific questions:

Hence this would mean that polymorphic type such as [a] are TYPE (i.e. *) and that the full name of the type is forall a. [a]

In other word, what i am after is to confirm that type declaration in haskell for polymorphic type are always in an abbreviated form, and that the full type name is always with an implicit forall a. ....

As I mentioned, I think this is not quite correct. Yes, [] at the type level needs a parameter to result in a type-of-terms; [] :: * -> *. So by definition 2, [] is not a type. However it's not really right to say that the full list type is "really" forall a. [a], as that is a specific type expression for universally polymorphic lists (which can only be the type of empty lists, or of lists full of bottom values, or a list that is the bottom value). In particular, [True, False] is a member of the type [Bool], and is not a member of the type forall a. [a].

Rather [] is just a type-level-entity of kind * -> *. whether you call that a type or not is up to you. Either way it is not the type of any terms, and either way it is a valid thing you can use in type expressions (provided they kind-check).

That is, in data Mytype a the type is not Mytype neither just Mytype a, but forall a. Mytype a, while Mytype is a type constructor.

It is true that Mytype is a type constructor. (In either definition of the word "type"; even if we're happy to call all type-level entities types, "type constructor" is still a specific category, and it's a good term to have because whether something is a "type constructor" cannot be determined just by looking at its kind, in the same way that you can't determine whether something is a data constructor just by looking at its type)

It is true that Mytype a on its own is not meaningful; it has to be used in a scope where a type variable a is in scope.

It is not true that forall a. Mytype a is the right way to think of "the type defined by data Mytype a. For any type a Mytype a is a type; forall a. Mytype a is a specific type expression that does not include most of the types we can form with the Mytype type constructor.

So any time you want to use Mytype a there will be a forall somewhere (either explicit or implicit). But it will usually be further out than immediately enclosing Mytype a; something like someFunc :: forall a. a -> Bool -> MyType a.

The OP left a comment on the other answer which I think it will be insightful to address:

I think I will edit the question, to explain where the all thingy of clarification is coming from. Let’s just say that while learning and experimenting with type classes, I was confused about instance Eq (a,b). Why not instance Eq (,), and the answer is not just because one need to refer to the type variable in the implementation. Eq can only be defined on a proper type, and any possible pair is actually a type, a polymorphic type. Then came the question, but what are we defining when we write data (,) a b = (,) a b . Am I defining (,) or forall a b. (a,b).

Keep in mind that making a type an instance of Eq is intended to mean that you can compare values of that type for equality.

When you say instance Eq (a, b) it really means instance forall a b. Eq (a, b); in English "for all types a and b, the type (a, b) is a member of the class Eq. It means you can pick any two types you like, apply the (,) type constructor to them, and the resulting type will be something use values you can compare for equality. (This is of course not actually true, the instance we really use is more like instance forall a b. (Eq a, Eq b) => Eq (a, b), because we need Eq a and Eq b)

instance Eq (,) is wrong because it is saying "the type constructor (,) is a member of the class Eq". "Values of (,) can be compared for equality" makes no sense, as (,) is not the kind of thing that can have values.

But (,) is still a thing that exists! And it's straightforwardly the thing defined by data (,) a b = (,) a b. It's just a thing with kind * -> * -> *, which is not the kind of thing we can make an Eq instance for. The phrase "Eq can only be defined on a proper type" is using the definition of "type" that only includes things with kind *, but remember "not being a proper type" by this definition does not mean "isn't a real thing", it just means we're choosing (in that particular sentence, at least) to use the word "type" with a narrow meaning. The class Eq is defined to have as members things with kind *, that's all. Other classes can be defined to have things with different kinds as members; if they have members of kind * -> * -> * then (,) on its own can be an instance of those classes. Have a look at the list of instances for Bifunctor, for example. The fact that the Eq instance has to be Eq (a, b) and not Eq (,) does not imply that (,) isn't "really" a valid entity that exists at the type level.

uj5u.com熱心網友回復：

宣言

data DatumType a b = Datum a b

宣告一種新型別 , DatumTypekind * -> * -> *。它還宣告了一個Datum型別為 的新術語forall a b. a -> b -> DatumType a b。

在正常情況下，型別簽名確實隱式地普遍量化了它們在頂層提到的所有型別變數。但是資料宣告不是型別簽名，因此您的問題的某些部分沒有意義。

在打開擴展的情況下，型別變數也可能是單態的，而不是普遍量化的。例如，

{-# LANGUAGE ScopedTypeVariables #-}

foo :: forall a. Monoid a => a -> a
foo x = mconcat xs where
    xs :: [a]
    xs = [x, mempty, x]

在此代碼片段中，所有量詞都已明確。在 where 塊內，xs具有單態 type [a]， wherea是由封閉型別范圍系結的型別變數，如果您插入了額外的量詞，則代碼將無法編譯：

foo :: forall a. Monoid a => a -> a
foo x = mconcat xs where
    xs :: forall a. [a]
    xs = [x, mempty, x]
    -- type error: can't match type a and type a0, whoops

有了這些資訊，希望你的每一個陳述的真實狀態更清楚，但讓我們一次過一遍：

我一直想知道型別是DatumType還是隱含 forall a. DatumType a b的。

無法回答。什么型別？DatumType和都是forall a. DatumType a b合法的型別級運算式。

這意味著像 [a] 這樣的多型型別是 TYPE 并且型別的全名是forall a. [a]。

有時。量詞的插入不是本地程序，而是整個型別簽名的全域程序。它們隱式地浮動到頂層。所以，這是兩種不同的型別：

-- these are all the same with ScopedTypeVariables off
forall a. [a] -> ()
forall a. ([a] -> ())
[a] -> ()

-- this is a different type from the ones above
(forall a. [a]) -> ()

So if, in normal, un-extended Haskell, you wrote the type signature x :: [a], then [a] would indeed be shorthand for forall a. [a]; but if you wrote the signature f :: [a] -> (), then [a] would not be shorthand for forall a. [a], because the forall has to be floated out from being on an argument to the arrow to being on the entire type.

In other word, what i am after is to confirm that type declaration in haskell for polymorphic type are always in an abbreviated form, and that the full type name is always with an implicit forall a. ....

Yes.

That is, in data Mytype a the type is not Mytype neither just Mytype a, but forall a. Mytype a, ...

Category error. data Mytype a is not a type signature, so there is no the type. If I were to single out a type to call "the type" from such a declaration, it would be Mytype alone, as that is the only type that gets created by the declaration.

...while Mytype is a type constructor.

Yes.

標籤：haskell

上一篇：Haskell-無法匹配型別

下一篇：當使用像“棱鏡”這樣的光學型別時，在“DerivingVia”期間無法強制