search

radeusgd / GADT-thesis

The repository containing Coq proofs attached to my master's thesis - Formal foundations for Generalized Algebraic Data Types in Scala
https://github.com/radeusgd/pDOT-GADT
0 stars 0 forks source link

Variable handling simplifications #6

Closed radeusgd closed 2 years ago

radeusgd commented 4 years ago

The original source language actually has two types of term variables: x-vars and f-vars.

x-vars are introduced by lambdas and f-vars are introduced by the fixpoint operator.

There is a slight difference in which ones can be used in places where a value is expected.

Currently the formalised calculus differs from that (for simplicity) in two ways:

It should be analysed and described how these changes influence the expressivity of the encoded language.

If we cannot prove on paper that expressivity is unaffected, the x/f-var distinction should be introduced.

Currently, it seems that it is not really related to the topic of GADTs, so my idea is to proceed with the formalization using the merged variables. If there is enough time after creating the language translation the problem can be revisited. It seems that the translation shouldn't be significantly affected by splitting these variable types (since if it works without the distinction, we just need to handle two branches instead of one and keep them as separate identifiers, but that is it).

My first intuition is that the only difference is in how we cannot return an x-var directly within a fixpoint or a type lambda (as they need a value and x isn't one), whereas in the original calculus we are able to do that.

image

(This explanation may need to be fleshed out a bit) But it seems to be an insignificant detail - since the forall type always brings an arbitrary type (so we have no type bounds) and ordinary functions do not bring new types into scope, we should be able to freely reorder big lambdas in relation to small lambdas, quantifying over types first and only then taking arguments - and in such scenario we do not need x-var to be treated as a value since the big-lambda will contain an ordinary lambda (which is itself a value) which does not need to contain a value, but arbitrary terms.

radeusgd commented 2 years ago

Afterwards, the lambda-variables and fix-variables have been split to more closely reflect the source calculus. The proofs have been updated to reflect the changes.