Open Rows

[gnumonik]

Related to #8, #4, and #6 because our choices there constrain our options here (& vice versa).

We need to figure out how to handle open rows. Well, kind of: In one sense, we don't need to worry about them at all, because all onchain scripts (Validators. MintingPolicies) necessarily lack any free type variables (I'm using "free" here to mean: No type variables at all, which isn't exactly right because a var bound by a quantifier is NOT free in the ordinary logical sense), and open row types get desugared to quantified expressions over a RowList.

Option 1: Defer Final Compilation Until All Types Are Instantiated

So option 1 for handling Open Rows is: We just don't. We defer final compilation into PIR or TPLC until we've already done all of the linking/inlining/etc on CoreFn, and only perform compilation into PIR or TPLC at a stage where it makes sense to throw an error if we encounter any Forall quantifiers. Note that while the type system used by PIR and TPLC does support quantification, I think that it is impossible to express the notion of a Row or RowList in those type systems. If a row type is closed, this doesn't matter, since we can translate rows (& operations on them) into products (& operations on them), and vice versa, using our access to field label information at compile time. If a row is open, however, we don't know the "size" of the product (in terms of # of args), which means we have no way to generate code for accessors and updates.

Concretely, "Ignore Open Rows" means:

• Our first compilation pass (which could accept an arbitrary number of modules) emits TypedCoreFn modules & externs files.
  • The main benefit here is that it allows users to write libraries & modules, & share/reuse code. I don't think we can support libraries/modules if we target PIR/TPLC instead of TypedCoreFn, because, as noted above, there are typed that we cannot really represent faithfully in PIR/TPLC given the limits of their kind system.
• Our second compilation pass (which targets a single function in a single module) performs inlining/linking/bundling/any CoreFn-level optimizations, working from the first-pass CoreFn modules, until we arrive at a closed CoreFn term
• We then translate CoreFn to PIR, perform additional optimizations, and error out if we encounter a "free" tyvar (because there shouldn't be any free tyvars at this point anyway).
• Finally, we compile PIR down to UPLC using IOG's (supposedly!) optimized compilation tools

Option 2: Desugar Open Rows to TypeClass Constraints

However, deferring final compilation until all quantified type variables have been instantiated with concrete types may unsatisfactory, and certainly constraints our choices w/r/t the other discussion items linked here. The defer-conversion-to-PIR approach basically forces us to output TypedCoreFn modules and do all of our "assembling" in TypedCoreFn. If we want to keep our options open, we could perform an additional desugaring step that transforms open rows into type class constraints.

Consider:

fun :: forall (r :: Row Type). {a :: Int, b :: Boolean | r} -> Int
fun r = if r.b then r.a else 0 

Semantically, {a :: Int, b :: Boolean | r} can be read as a constraint that is satisfied by any row p such that p has unique labels, p .! a ~ Int and p .! a ~ Boolean, where .! is read as lookup . (I note in passing that this is how things work in the Haskell row-types library). This is something that we can express with a type class, something roughly like (ignoring uniqueness for a moment):

class HasType :: Symbol -> Type -> Row Type -> Constraint 
class HasType l t r | l r -> t where 
   lookup :: Record r -> t   -- will require a type application to use, could also pass proxies 

This would probably be a compiler-solved typeclass that only a closed row can satisfy. (Actually, I think any inductive typeclass over rows is, necessarily, only satisfied by closed rows?)

The original example could then be desugared to:

fun :: forall (r :: Row Type)
        . HasType "a" Int r 
     => HasType "b" Boolean r
     => Record r 
     -> Int 
fun r = if lookup @"b" r then lookup @"a" r else 0  

Despite appearances (i.e. the presence of a tyvar of kind Row Type), we should be able to generate code from this that "forgets" the type. Morally, this is:

fun :: forall (t :: Type)   -- Type is OK, PIR/TPLC have "Type" 
        . (t -> Int) 
     -> (t -> Bool)  
     -> t 
      -> Int 
fun dictA dictB r = if dictB r then dictA r else 0 

While this approach gives us flexibility, it has some drawbacks:

• The desugaring process would be complicated & error prone
• It'll necessarily carry a performance penalty
• In order to actually apply the dictionary args, we'll likely have to add some PS type information to the PIR/UPLC ann annotation. At the very least, we need to preserve the mapping of labels to types, since the label is necessary for solving the constraint/instantiating the dictionary. (Honestly, probably more than just that, this will be complex

Overall, I think that Option 1 is preferable if it doesn't cause too many issues elsewhere. I suspect that it will be easier to perform optimizations (especially a "minimize the number of times we traverse the same record" optimization) with that approach, which would be very difficult with Option 2.

But, again, Option 1 locks us into a certain way of handling linking/bundling/etc, so it's worth keeping the alternative in mind. We should minimize overall complexity and confusion, which may require accepting more of it here to balance out concerns elsewhere.

[GeorgeFlerovsky]

deferring final compilation until all quantified type variables have been instantiated with concrete types may unsatisfactory

Why would it be unsatisfactory?

This approach gives us flexibility?

Flexibility to do what? Why would we want it?

[klntsky]

@GeorgeFlerovsky

Why would it be unsatisfactory?

It is satisfactory for us. We always target a single function in the end. Per-module compiling is useful to have incremental builds, but it does not matter which representation we cache.

Flexibility to do what? Why would we want it?

To support open rows without letting them "leak" down the language hierarchy. I think we can give up this flexibility as 1 is clearly the better option.

Slightly related: #2

[klntsky]

Hmmm, so,

f :: forall r. { b :: Int | r } -> Int
f { b } = b

main = f { b: 1, a: "foo"} + f { b: 2, c: 3 }

would require us to generate two PIR functions, essentially we would treat every row type parameter like C++ treats template parameters.