Amend #281 (visible forall) and #378 (Design of DH) to clarify treatment of term variables in types

[JakobBruenker]

Say you have

x :: Natural
x = 4

f :: forall (n :: Natural) -> ()
f _ = ()

main :: IO ()
main = pure (f (type x))

Here, we're passing the term variable x as argument to f, which expects a type. Is this allowed? #281 says

9. Any uses of terms in types are ill-typed

so the answer is no.

But it also says

In the type checking environment, the variable must stand for a type variable, or else it treated as a fresh skolem constant.

...so the answer is yes?

In a brief discussion in GHC issue #23717 we agreed that this particular aspect of #378 can wait until a later proposal.

Update: We also use this opportunity to expand somewhat on the explanation of term variables in types in #378.

[JakobBruenker]

ping @int-index

[simonpj]

Concerning

x :: Natural
x = 4

f :: forall (n :: Natural) -> ()
f _ = ()

main :: IO ()
main = pure (f (type x))

I think that should be rejected. The binding for x could easily have been

x = f 33

where f is some arbitrarily complicated function, which the type checker would have to evaluate. The current DH design just doesn't allow that.

So I like this:

• Any uses of terms in types are ill-typed

and I don't like this

• In the type checking environment, the variable must stand for a type variable, or else it is treated as a fresh skolem constant

Now, it is true that GHC proposal #378: design for Dependent Haskell says in Section 4.6:

• The examples above include applications to variables. These variables will be treated exactly as skolems at compile-time, even if they are let-bound with known right-hand sides.

which suggests that we accept the above program but without exploiting the knowledge of what x is bound to. But that proposal does not justify why that is a good idea or what value it would bring. Why not just reject it?

[JakobBruenker]

Copying my comment from #23717 which I think addresses that point:

Imagine you have

foo :: foreach (str :: String) -> <some type involving str>
foo str = ...

main :: IO ()
main = do
  str <- readLine
  let result = foo str
  ...

Here, we want to use a function that uses foreach with data we only get at runtime. But to do this, we need to be able to pass a term variable to this function. (Since, contrary to the example with x = 4, we can't just construct a type that mirrors the term - we don't know yet what the term will be.)

The way singletons handles this is with a function called toSing which produces an existential value containing a singleton. So there is some symmetry here between singletons using an existential, and DH using a skolem.

[int-index]

First of all, I support the amendment. The proposal shouldn't contradict itself. Thank you @JakobBruenker for spotting this problem!

There are two ways to resolve the contradiction:

1. Remove the skolem clause (as this amendment does)
2. Rewrite other parts of the proposal to respect the skolem clause

Simon expresses skepticism about the usefulness of option 2. I don't share this skepticism; on the contrary, I am rather excited about the possibility to mention term-level variables at the type level. The example in @JakobBruenker's last comment has the right idea. I can offer a similar example, a bit more concrete:

vReplicateA :: Applicative f => foreach (n :: Nat) -> f a -> f (Vec n a)
vReplicateA Z _ = pure VNil
vReplicateA (S n') act = liftA2 VCons act (vRelicateM n' act)

vZip :: Vec n a -> Vec n b -> Vec n (Tuple2 a b)
vZip VNil VNil = VNil
vZip (VCons x xs) (VCons y ys) = VCons (x, y) (vZip xs ys)

mkInt :: IO Int
mkBool :: IO Bool
h :: Vec n (Tuple2 Int Bool) -> IO Unit

main = do
  let n :: Nat
      n = ...   -- or a monadic bind (n <- ...) if you will
  intVec <- vReplicateA n mkInt
  boolVec <- vReplicateA n mkBool
  h (vZip intVec boolVec)

In main, the vZip intVec boolVec call will type check only if we know that both intVec and boolVec have the same length. And we do know that – their length is determined by the term-level variable n introduced in a local let-binding. The right-hand side of the binding is not important at all.

Note that this example also relies on vReplicateA being able to pattern match on the n passed to it. Pattern matching is what allows us to perform useful computation even if we don't look at the RHS of the binding

So #378 has this skolem clause for a good reason. But should it be in #281? I can't think of a useful example that would use forall, not foreach. So I don't think that #281 is the right place to introduce this. I'm quite content to save it for later.

[simonpj]

Simon expresses skepticism about the usefulness of option 2. I don't share this skepticism; on the contrary, I am rather excited about the possibility to mention term-level variables at the type level.

OK I'm convinced. Thank you for explaining so patiently.

I can't think of a useful example that would use forall, not foreach

That is a very helpful insight.

My conclusion

• Yes I support amending Visible forall in types of terms, and types in terms #281 (dropping the "skolem" bit for term variables in types), but leaving the full vision in Support the design for dependent types #378 as it is (i.e. retaining the "skolem" bit for term variables in types)
• BUT I would like to see this actually explained, in a way that is not just buried deep in a discussion thread of a PR (this one) that modifies a proposal Visible forall in types of terms, and types in terms #281 that itself implements part of a vision Support the design for dependent types #378.

To be constructive, how about this:

• Add to this PR a change to Support the design for dependent types #378, by adding a whole new subsection of Section 4, to explain the role of term variables in types. It belongs with 4.5 which is about foreach. This could give your example above, and explain the importance of a "skoelm" term variable in a type.
• Also in Support the design for dependent types #378 change the brief mention of skolems in 4.6 to point to the new subsection -- thereby explaining the otherwise-mysterious " These variables will be treated exactly as skolems at compile-time, even if they are let-bound with known right-hand sides."
• Augment the amendment (in the MR) to Visible forall in types of terms, and types in terms #281 so that it points to the new subsection in Support the design for dependent types #378 and explains why we don't need the skolem thing becasue we don't have foreach.

Then our future selves, reading these proposals, will be able to make sense of it all. Thanks!

@rae may have a view.

[JakobBruenker]

(wrong @rae, you presumably meant to ping @goldfirere)

[JakobBruenker]

Regarding your suggestions @simonpj, I agree, I will change the PR accordingly.

[JakobBruenker]

I've made the changes @simonpj suggested.

[simonpj]

Note that to demonstrate why this is useful, we had to use a function (vReplicate) that uses the retained quantifier foreach.

thanks. But can you add a corss ref here saying "(see Section 4.5)"? Because vReplicate is indeed set out there, complete with the foreach. Ah.. I see that "dependent pattern match" links to that section, which is also fine. But if I'm reading I may not even get to that sentence before trying to figure out what vReplicate is and why it uses foreach.

Also I stumbled on "retained quantifier". Actually this in in 4.4 but I'm not famililar with the terminology. So lets have:

• "Note that to demonstrate why this is useful, we had to use a function (vReplicate), defined in Section 4.5, that uses the retained quantifier foreach (see Section 4.4 on quantifiers)."

[JakobBruenker]

Sounds good, I've made that change (slightly adapted because I can't figure out how to make a working link where section name and link text differ)

[JakobBruenker]

@nomeata I think this is ready to go to the comittee. CC @int-index

[simonpj]

I'm in support. Helpful clarification.