Escaping ADTs and typability

[jaccokrijnen]

Problem

What is the type of this PIR program?

  let data Bool = True | False in 
  True

It can't be Bool, because it is not "in scope" outside the let.

Apparently, such programs are/were allowed in the plutus compiler, and the resulting PLC term is "fine" and typeable:

  (ΛBool. λTrue. λFalse. True) {Bool} {True} {False}

where {⋅} is the Scott encoding of the type/constructor.

It is problematic, because the intermediate PIR program is not typeable. This can be seen from the typing rules in the "Unraveling Recursion" paper.

From discussion [1] (also in file Transform/ScottEnc/iog-discussion), I learned a few things:

• There was work on implementing a PIR type-checker.

• The problem was: the compiler accepted programs with escaping data types, which would not type-check in PIR. (presumably, the type-checker being implemented was going to be used for a sanity check in the compiler, similar to what GHC does with core)

• Michael wrote several possible solutions. The most important one being to reject such programs and therefore only allow programs that have a built-in type at top-level ( ->, unit and Data (in the future)).

• Phil was in favor of that approach.

• The unraveling paper prevents escaping types by the premise Γ ⊢ T :: *
  in the rule of T-Let(Rec)

• There is a conceptual mismatch in scoping between Haskell and PIR:

  • Haskell has one "global" top-level scope for data definitions
  • PIR only has locally scoped datatypes

• Roman argued that a type-checking Haskell program compiles into a non-type-checking PIR program, which compiles into a type-checking PLC program (because of scott-encoding).

• Roman proposed a PIR type-checking algorithm, which would accept the
  programs with escaping types, basically by ignoring the type of let data constructs, and just type checking the body and kind checking the definition.

  • Q: How would `(\x -> .... ) (let data A = A1 in A1) be typechecked?

• It looks like there was not enough interest to implement this idea, and the solution of rejecting programs with escaping types seems simpler.

Conclusion: in plutus-cert, we could only certify the case of non-escaping types.

Joris mentioned escaping gives problems in lemmas like substitution_preserves_typing.

Q: what is the actual status in the PIR compiler?

[1] https://groups.google.com/a/iohk.io/g/plutus/c/2MAHb6uP3y0/m/vB0sssjCAwAJ?utm_medium=email&utm_source=footer&pli=1

[jaccokrijnen]

Currently, the PIR compiler does not allow escaping type variables, except on the top-level [1]. I think we can add this in the typing rules by adding one "wrapper" relation that handles the top-level let. Within the has_type relation we just require that ADT T does not occur in the let-body's type.

However, in the logical relation we might have a bit of a problem, because there would be a distinction between arbitrary expressions and the top-level expression. Does a top-level expression ("program") have a different definition for RC, RV etc? What are values for "programs"? Expressions of the form let data ... ; ... data ... in v? Where v is a regular value?

We can start with ignoring the top-level typing exception, and just disallow any type-variable escaping. On the top-level, a plutus contract will have to return at least a Bool though (or a () when using the translation from Bool to error or ()).

[1] https://github.com/input-output-hk/plutus/blob/ec1540a2da65280002f5877c64cda3480b81edef/language-plutus-core/docs/Typechecking%20PIR.md

[jaccokrijnen]

This is how the current typing rules in coq disallow shadowing:

  | T_Let : forall Δ Γ bs t Tn Δ' Γ' bsGn,
      Δ' = flatten (map binds_Delta bs) ++ Δ ->
      map_normalise (flatten (map binds_Gamma bs)) bsGn ->
      Γ' = bsGn ++ Γ ->
      Δ ,, Γ |-oks_nr bs ->
      Δ' ,, Γ' |-+ t : Tn ->
      Δ |-* Tn : Kind_Base ->
      Δ ,, Γ |-+ (Let NonRec bs t) : Tn

Specifically, the premise Δ |-* Tn : Kind_Base requires Tn to be typable under the global context $\Delta$.