search

lpw25 / girards-paradox

A "implementation" of Girard's paradox in OCaml
104 stars 2 forks source link

Are you able to extend this to make the type checker diverge? #1

Open monsanto opened 9 years ago

monsanto commented 9 years ago

In the dependent type:type calculus there is way to modify Girard's paradox to exhibit a diverging type (as opposed to a diverging term). There is some information on this in this 1989 paper by Reinhold: ftp://129.69.211.95/pdf/mit/lcs/tr/MIT-LCS-TR-458.pdf (EDIT: apparently GitHub markdown doesn't like ftp links). It would be interesting to know if this is possible to do in OCaml; for example, it isn't possible in System U.

Of course it is well known that the OCaml subtyping relation is undecidable in the presence of abstract module types, so for this to be interesting the example would need to avoid making use of that fact.

lpw25 commented 9 years ago

It would be interesting to know if this is possible to do in OCaml; for example, it isn't possible in System U.

I do not believe it to be possible in current OCaml. The reason that the type does not diverge is that at various points the type is abstracted, which hides the underlying equalities and prevents the type-checker from doing further beta reduction. Many of the abstractions in this code were explicitly inserted for readability, but even if all of them were removed there are some places where OCaml currently forces abstraction on you. For example:

modulde F (X : S) = struct
  module Y = X
end

is given type:

module F (X : S) : sig
  module Y : S
end

which hides the equality between Y and X. If/when OCaml's module aliases are extended to work with functor arguments/results such that F had type

module F (X : S) : sig
  module Y = X
end

then I believe it would be possible to produce a diverging type.

Of course it is well known that the OCaml subtyping relation is undecidable in the presence of abstract module types, so for this to be interesting the example would need to avoid making use of that fact.

Whilst I have no strong evidence for this, I believe the two issues are related: I have never seen an example of the subtyping relation diverging that would not have been prevented by having a predicative universe of module types.