We know that

forall a. a -- undefined
forall a. [a] -- [] or undefined
forall a. (a,a) --  undefined

However i have noticed that

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

That is record :: forall a. Record a is not undefined as in the above. 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.

The above first quantification are well explained here:

• What is the difference between forall a. [a] and [forall a. a]?
• Which is a polymorphic type: a type or a set of types?

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 ? How is GHC actually handling it ?

CodePudding user response：

In general, if:

data Record a where
    Record :: forall b. { field :: Whatever b } -> Record b

for an arbitrary type function Whatever, then forall a. Record a will be inhabited (by a non-bottom value) if and only if forall a. Whatever a is inhabited.

This shouldn't be too surprising. This single field ADT creates a polymorphic isomorphism between Record b and Whatever b through the functions Record and field:

Record :: forall b. Whatever b -> Record b
field :: forall b. Record b -> Whatever b

and the rules of rank-2 types allow the following isomorphism -- between the inhabitants of forall a. Record a and forall a. Whatever a -- to type check:

toRecord :: (forall a. Whatever a) -> (forall a. Record a)
toRecord = Record

fromRecord :: (forall a. Record a) -> (forall a. Whatever a)
fromRecord = field

Note that the field doesn't need to be a function. Given:

data Record1 a where
    Record1 :: forall b. { field1 :: [b] } -> Record1 b

the type forall a. Record1 a is isomorphic to forall a. [a] and is inhabited by Record1 [].

Maybe that helps?

CodePudding user response：

We know that

forall a. a -- undefined
forall a. [a] -- [] or undefined
forall a. (a,a) --  undefined

Yes, but also these:

• forall a. [a] contains:

  1. undefined
  2. [] (fully defined)
  3. undefined : xs for any xs:
  • undefined : [], a.k.a. [undefined]
  • undefined : undefined : undefined
  • undefined : undefined : [], a.k.a. [undefined, undefined]
  • (And so on.)

• forall a. (a, a) contains no fully defined terms:

  1. undefined
  2. (undefined, undefined)

However i have noticed that

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

That is record :: forall a. Record a is not undefined as in the above.

That’s right. forall a. Record a contains the terms:

1. undefined
2. Record undefined, a.k.a. Record { idx = undefined }
3. 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:

• Void has 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 term undefined.

• Either A B is inhabited by Left (x :: A) and Right (y :: B), if either A or B (or both) are inhabited. It contains undefined, Left undefined, and Right undefined as well.

• (A, B) is inhabited by (x :: A, y :: B) if both A and B are inhabited. It contains undefined, (x, undefined), (undefined, y), and (undefined, undefined) too.

• A -> B is inhabited if it can construct a value y :: B for each value x :: A.

• forall (x :: J). (Y :: K) is inhabited if it can construct a type Y :: K for each type x :: J (where J and K are kinds, like Type, 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]).