我們知道
forall a. a -- undefined
forall a. [a] -- [] or undefined
forall a. (a,a) -- undefined
但是我注意到
data Record a where -- GADTSyntax eq. to data Record a = Record { idx :: a -> a }
Record :: forall b. {idx :: b -> b } -> Record b
record :: forall a. Record a
record = Record { idx = \x -> x } -- Not undefined
這record :: forall a. Record a不是像上面那樣未定義。我懷疑這是因為它是函式的記錄，但這并不能真正解釋為什么就型別系統的規則而言這是可以的。
上面的第一個量化在這里得到了很好的解釋：
- forall a 和有什么區別？[a] 和 [forall a. 一種]？
- 哪個是多型型別：一個型別還是一組型別？
因此，我想知道是否有人可以提供一些“有點”“正式”（型別系統透視解釋）來說明這怎么可能，即實際發生了什么？GHC實際上是如何處理它的？
uj5u.com熱心網友回復：
一般來說，如果：
data Record a where
Record :: forall b. { field :: Whatever b } -> Record b
對于任意型別的函式Whatever，則forall a. Record a當且僅當被居住時才會被居住（由非底部值）forall a. Whatever a。
這應該不足為奇。Record b這個單一欄位 ADT 在函式之間和Whatever b通過函式Record和創建多型同構field：
Record :: forall b. Whatever b -> Record b
field :: forall b. Record b -> Whatever b
并且 rank-2 型別的規則允許以下同構——在 和 的居民之間forall a. Record a——forall a. Whatever a進行型別檢查：
toRecord :: (forall a. Whatever a) -> (forall a. Record a)
toRecord = Record
fromRecord :: (forall a. Record a) -> (forall a. Whatever a)
fromRecord = field
請注意，該欄位不必是函式。鑒于：
data Record1 a where
Record1 :: forall b. { field1 :: [b] } -> Record1 b
該型別forall a. Record1 a與 同構forall a. [a]并且由Record1 [].
也許這有幫助？
uj5u.com熱心網友回復：
我們知道
forall a. a -- undefined forall a. [a] -- [] or undefined forall a. (a,a) -- undefined
是的，還有這些：
forall a. [a]包含：undefined[]（完全定義）undefined : xs對于任何xs：
undefined : []，又名[undefined]undefined : undefined : undefinedundefined : undefined : []，又名[undefined, undefined]- （等等。）
forall a. (a, a)不包含完全定義的術語：undefined(undefined, undefined)
但是我注意到
data Record a where -- GADTSyntax eq. to data Record a = Record { idx :: a -> a } Record :: forall b. {idx :: b -> b } -> Record b record :: forall a. Record a record = Record { idx = \x -> x } -- Not undefined這
record :: forall a. Record a不是像上面那樣未定義。
這是正確的。forall a. Record a包含以下條款：
undefinedRecord undefined，又名Record { idx = undefined }Record id, a.k.a.Record { idx = id }, which is a defined value
I suspect it is because it is a record of functions, but that does not explain really why with respect to the rule of the type system this is ok.
Not exactly. GADTSyntax gives the type of the constructor explicitly, which is a good starting point to understand this. We have:
Record :: forall b. { idx :: b -> b } -> Record b
Or, without the record notation, and with some extra parentheses and a KindSignatures annotation for good measure:
Record :: forall (b :: Type). ((b -> b) -> Record b)
That is to say, if you apply the data constructor Record to any Type argument of your choosing, then it will be assigned to the type parameter b and substituted into the type (b -> b) -> Record b. For example, with Int:
forall b. (b -> b ) -> Record b
(b ~ Int) => (b -> b ) -> Record b
(Int -> Int) -> Record Int
(NB. ~ is an equality constraint; this syntax is enabled by the GADTs or TypeFamilies language options.)
This parallels how a lambda/function expression receives an argument value for its parameter:
(\ i -> i 3)
let i = 2 in i 3
2 3
In fact, forall is the type-level analogue of a lambda, it just takes and produces types rather than values.
So, after applying Record to a type b, if you apply the result to a function f :: b -> b which accepts and returns values of that particular type b, then you can construct a value of type Record b (here, the type constructor Record). Normally, the application of type arguments is implicit, but you can make it explicit with the TypeApplications language option:
Record :: forall b. (b -> b ) -> Record b
Record not :: Record Bool
Record @Int :: (Int -> Int) -> Record Int
Record @Int (* 2) :: Record Int
Now, in the polymorphic case, record :: forall a. Record a, you’re saying that anyone is free to supply record with any type a that they choose (such as record @Char) and they’ll get back a value of type Record a (being Record Char if a = Char). Except for the extra Record wrapper, this is the same as promising to construct T -> T for each possible type T, and in the general case, that’s promising T -> T for all T, because record doesn’t demand any further information constraining its type parameter, like Num a or Ord a.
With the ScopedTypeVariables language option, you can annotate the fact that, inside the body of record, there’s a particular type variable called a, whose value is unknown to you, but nevertheless constant.
{-# Language ScopedTypeVariables #-}
-- ‘forall’ defines the scope of ‘a’.
record :: forall a. Record a
-- ‘a’ refers to the above ‘a’, not a new one.
record = Record { idx = \ (x :: a) -> x }
Or:
{-# Language ScopedTypeVariables #-}
record :: forall a. Record a
record = Record { idx = f }
where
-- Again this would normally mean a fresh ‘a’,
-- but here it refers to the scoped ‘a’.
f :: a -> a
f x = x
Hence I wonder if anyone can provide some "somewhat" "formal" (type system perspective explanation) clarification of how is that possible i.e. what is actually happening ?
Another way to think of this is that, if a type contains only terms that can be fully evaluated to values, then interpreting that type as a logical formula (by the Curry–Howard correspondence) will produce “true”, i.e. it will be a tautology; if it’s “false”, then a term of that type must crash or loop in some cases, like head [], but not necessarily all cases, like head [1]. You can look at this very mechanically:
Voidhas no values, since it has no constructors. This corresponds to “false”. It contains only one term,undefined.()has one defined inhabitant for its one constructor, and corresponds to “true”. It also contains the termundefined.Either A Bis inhabited byLeft (x :: A)andRight (y :: B), if eitherAorB(or both) are inhabited. It containsundefined,Left undefined, andRight undefinedas well.(A, B)is inhabited by(x :: A, y :: B)if bothAandBare inhabited. It containsundefined,(x, undefined),(undefined, y), and(undefined, undefined)too.A -> Bis inhabited if it can construct a valuey :: Bfor each valuex :: A.forall (x :: J). (Y :: K)is inhabited if it can construct a typeY :: Kfor each typex :: J(whereJandKare kinds, likeType,Type -> Type, &c.).Other types can be expressed as (possibly recursive) combinations of these primitive ones.
So for example forall a. a is false, because if you interpret it as a logical expression (“for all A (true or false), A is true”) then it obviously has a counterexample (“false is true” is nonsense).
forall a. Record a (or just forall a. a -> a, without the wrapper) are inhabited because you can always produce Record id (resp. id). Logically this is saying “for all A, A implies A”, which is the case: truth implies truth, and falsehood implies anything (a.k.a. ex falso quodlibet).
Likewise, forall a. [a] is inhabited because you can always produce []. In detail, this is the logic formula “L(A) = for all A, true or L(A)”, which is always true, derived by unrolling [a] into Either () (a, [a]), with () corresponding to [] :: [a], and (a, [a]) corresponding to (:) :: a -> [a] -> [a]).
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/450280.html
下一篇：GADT的索引初始代數