Resolve remaining issues with `ifix` about plutus

[BekaValentine]

@michaelpj in generally, it's preferable to have connectives be "pure", i.e. not defined in terms of one another, b/c it makes type systems more modular. the proofs of various properties aren't too tightly intertwined. in the case of ifix, i think there's no real avoiding it, however, so we might as well just go all out and make it a fully saturated non-binder

[effectfully]

It's not clear to me that it's easier to debug.

Right.

Plus then we have two implementations that have to both be correct.

I want to check them against each other using property testing.

Well, I guess you're right, syntactic packing only increases maintenance burden, so I'll remove it (after a little bit more thinking just in case).

[effectfully]

How do we call ifix? I've just looked into the spec and ifix is called fix there. I'm opposed to that, because I use this name for the generic fix :: (k -> k) -> k. This matters a lot for documentation, because you either get a terrible ambiguity if both things are called equally or need to call the generic fix some other name, but that fix is what actually used in comments, e.g.:

list = fix \(list :: * -> *) (a :: *) -> all (r :: *). r -> (a -> list a -> r) -> r

so I do want it to have the default name. ifix does not leak to the user, we provide an API that looks like we have the generic fix. And ifix is a very particular form of a fixed point combinator, I believe it deserves some specificity in its name.

[effectfully]

Should it be saturated?
i.e. ifix f :: k -> * vs ifix f a :: *

I think we agree it should be saturated?

Should it be a binder?
We could bind the argument of the pattern functor, and also the argument if it's a saturated form.

I tried that and it was a pain. That's what I posted in the PR that adds ifix:

There are three cases here:

1. fix binds no variables
2. fix binds the pat variable
3. fix binds the pat and the arg variables

I tried to do as fewer changes as possible, so my first attempt was (2). This resulted in code like this:

        TyIFix a tn ty arg -> do
            clonedArg <- clone what arg
            addBound (tn ^. unique)
            TyIFix a <$> clone what tn <*> clone what ty <*> pure clonedArg

I.e. we need to clone arg before cloning pat, because the latter requires adding a bound variable to scope which is not bound in arg. That's not too much trouble, but is not nice.

Then in type rules we need to interleave function application with explicit substitution. This is ugly and harder to read than necessary. This is how the unwrap rule looks like:

-- [infer| term : ifix n vPat vArg]
-- -----------------------------------------------------------
-- [infer| unwrap term : NORM (([ifix n vPat / n] vPat) vArg)]

I consider

-- [infer| term : ifix vPat vArg]
-- ---------------------------------------------------
-- [infer| unwrap term : NORM (vPat (ifix vPat) vArg)]

much more readable. And why would we bind one variable and not the other?

I haven't tried (3), but it has to be very bloated: two variables each of which has a name and a type. And every single function that matches on TyFix has to handle two binders. This is just boilerplate.

However there is another reason why I prefer not to make Fix a binder: because it's not a binder in all of the several dozens of Agda files I've produced so far. It has been a constant pain for me to convert something I wrote in Agda to PLC due to the need to perform that binding twist in my head. The same applies to type rules: I write them pretending fix is not a binder and then adapt to fix-as-a-binder setting. I think fix being not a binder is easier to reason about, especially when fix binds two variables

So with respect to implementation, making ifix a binder is just a pain: it complicates code, it complicates rules, it complicates conversion from Agda (which is very important, because I have really complicated encodings there which would be very hard to write by hand without the Agda assistance), it impedes my reasoning. I have functions there like this:

-- | Pack an n-ary pattern functor of kind @k -> k@ into a 1-ary one of kind
-- @((k -> *) -> *) -> (k -> *) -> *@
--
-- > \(withSpine :: ((k -> *) -> *) -> k) (patF :: k -> k) ->
-- >     \(rec :: (k -> *) -> *) (spine :: k -> *) -> spine (patF (withSpine rec))
packPatternFunctorN ann k withSpine patF = do
    rec   <- freshTyName ann "rec"
    spine <- freshTyName ann "spine"
    let star  = Type ann
        (~~>) = KindArrow ann

    return
        . TyLam ann rec ((k ~~> star) ~~> star)
        . TyLam ann spine (k ~~> star)
        . TyApp ann (TyVar ann spine)
        . TyApp ann patF
        . withSpine
        . TyApp ann
        $ TyVar ann rec

And this is just one function, I have several functions like that. Originally, I kept everything on the Plutus Core side, but that resulted in huge unreadable terms, so I decided to pass some arguments via Haskell lambdas rather than Plutus Core lambdas, because this way we can actually reduce types on the Haskell side rather than collect redexes on the Plutus Code side. In the function above I'm mixing the two levels and pass some stuff via Haskell lambdas and some via Plutus Core lambdas. It's already complicated, but at least I only move lambdas back and forth between the source and the target language, so it's pretty mechanical. But adding implicit scope extensions would be a nightmare, because then I also need to keep track of those extensions in my head and move back and forth between scope extensions and lambdas as well.

I've described the reasons not to make ifix a binder, what are the reasons to make it a binder?

Are there problems with preserving the normalization status of "multi-argment" pattern functors when we encode them into our unary version? (Not sure if I got that right, hopefully @effectfully can elaborate)

There are. I'm solving them. Docs (including an explanation of what the problem is) are on the way.

I believe the current state of the syntax is:

I believe the same.

[jmchapman]

@psygnisfive made a well motivated argument that mu should be a binder which as I understand it is because as we want to minimise connectives being dependent on each other.

G !- B => K
G, r :: K -> *, t :: K !- A => *
--------------------------------
G !- ifix(B; r,t.A) => *

However, this still needs to refer to the -> so this cannot be achieved completely.

I have an argument for the opposite: We can take a 'logical framework' approach. The lambda and application are 'meta' and the other stuff (pi and mu) are object level/language specific. We have one binder - lambda, and we use that whenever we need to bind a variable.

We can define mu as:

μ1 : ∀{φ K} → φ ⊢⋆ ((K ⇒ *) ⇒ K ⇒ *) ⇒ K ⇒ *

and, indeed, we could do the same for pi:

Π : ∀ {Φ K} → Φ ⊢⋆ (K ⇒ *) ⇒ *

I think all the versions should be equivalent, so I don't think it is a huge problem. Also, I think the iso- vs. equi- recursive type discussion is orthogonal, the fact we could have this discussion about pi only which adds to this.

I still don't understand the saturation argument. In the Agda formalisation wrap and unwrap are saturated and the builtin constructor is guaranteed to be saturated - it has to have exactly as many arguments as are specified in the signature. I do understand the need to wait until the builtin has enough arguments (and indeed then computing them all to values) before trying to compute it. I don't see the connection between saturation at the term level and saturation at the type level. But, perhaps this is a difference between the Haskell/Agda implementations.

In summary, I think we have a relatively free choice and so far I think @effectfully and I have chosen the path of least resistance from an implementation perspective. I think one can make different arguments from a language design perspective, @psygnisfive and I have made two, there are perhaps others.

[michaelpj]

I'm not sure I really understand the motivation for wanting to reduce how much mu depends on ->. Is the idea that we could use a binder-mu in a language without higher kinds? Much like we can have forall without higher kinds, whereas James' binder-free version of forall requires them?

Of course, as James points out, we can't actually get to that point with ifix, because we still have a kind arrow even in the binder version. Does that negate all the benefit, or is it still helpful to go part way?

[effectfully]

Here is another argument in favour of not making ifix a binder: often I separate definitions of pattern functors from definitions of actual data types. And sometimes pattern functors are computed rather than just written down. For example, in one of our docs we have

treeForestF =
    \(a :: *) (rec :: (* -> * -> *) -> *) (tag :: * -> * -> *) -> all (r :: *).
        tag ((a -> rec forestTag -> r) -> r)                  -- `case` over `tree`
            (r -> (rec treeTag -> rec forestTag -> r) -> r))  -- `case` over `forest`

Here treeForestF, being applied to an a, computes to a pattern functor. And it's not just for convenience, it's really a reusable and meaningful part of the encoding of the tree/forest family, because later we have

tree   = \(a :: *) -> ifix (treeForestF a) treeTag
forest = \(a :: *) -> ifix (treeForestF a) forestTag

How to do the same in the ifix-as-a-binder setting?

[effectfully]

Okay, here is another bunch of ifix-related documentation, this time implementation-specific. It also describes the denormalization problem, a possible (already implemented) solution and enumerates pros and cons of this approach (and the old one with non-normalized types). Do not read the actual code there, only the docs.

[michaelpj]

@effectfully I've read what you wrote about the denormalization problem. I'm not sure I'm convinced that it's a problem we need to solve. As I understand it, the problem is that a user of the Plutus Core library (i.e. someone programmatically generating Plutus Core) might feed in a normalized n-ary pattern functor and get out a type that is non-normalized.

But as someone generating Plutus Core programmatically, it doesn't seem that important to me to preserve normalization in this way. For one thing, tracking whether or not I'm preserving normalization is a pain (to be in this situation you are assuming I already know and care whether the pattern functor is normalized!). For another thing, if I actually do care about the types in my program being normalized, I can just normalize them afterwards!

So I think either:

• The user cares about types being normalized. They can just normalize them afterwards (and will probably want to do so regardless, to be sure).
• The user does not care about types being normalized. No problem.

So my vote is that we shouldn't care and we should just do the "semantic" packing.

[effectfully]

@michaelpj, I completely agree with everything.

Some thoughts:

• it's still good to have this "denormalization" thing being documented (including the motivation of why we're not preserving normalization when we can), because it's kind of a "surprise"
• it's still good to be able not to add additional redexes and not to remove supplied ones, because I actually debug things by looking at Plutus Core from time to time

So if people think it's fine, I'm going to keep the docs and the "syntactic" packing, but only use "semantic" packing for production.

[michaelpj]

Yes, we should certainly document it.

I don't see why you want to keep the "syntactic" packing, though? It's not clear to me that it's easier to debug. Plus then we have two implementations that have to both be correct.

[wadler]

re: plutus/language-plutus-core/stdlib/Language/PlutusCore/StdLib/Type.hs
[Note: Denormalization]

I cannot read lines 218--225, despite the claim on the next line that it is "pretty readable (once you know how to read it)". Can you explain to me how to read it?

255-256: "Then the question is whether it's possible to preserve redexes in user-written types and not to
produce new ones while encoding the types." Why is this question of interest?

[wadler]

Here is another argument in favour of not making ifix a binder: often I separate definitions of pattern functors from definitions of actual data types. And sometimes pattern functors are computed rather than just written down. For example, in one of our docs we have

treeForestF =
    \(a :: *) (rec :: (* -> * -> *) -> *) (tag :: * -> * -> *) -> all (r :: *).
        tag ((a -> rec forestTag -> r) -> r)                  -- `case` over `tree`
            (r -> (rec treeTag -> rec forestTag -> r) -> r))  -- `case` over `forest`

Here treeForestF, being applied to an a, computes to a pattern functor. And it's not just for convenience, it's really a reusable and meaningful part of the encoding of the tree/forest family, because later we have

tree   = \(a :: *) -> ifix (treeForestF a) treeTag
forest = \(a :: *) -> ifix (treeForestF a) forestTag

How to do the same in the ifix-as-a-binder setting?

Wouldn't it just be the same, only now we pass the two arguments to the saturated form of ifix rather than use function application?

[effectfully]

@wadler,

I cannot read lines 218--225, despite the claim on the next line that it is "pretty readable (once you know how to read it)". Can you explain to me how to read it?

Added a couple of more notes. Inlining them here:

{- Note [Generic fix]
Now that we know how to pack n-ary functors into 1-ary ones
(see [Packing n-ary pattern functors semantically]), only a few tiny steps remain to get the generic

    fix :: (k -> k) -> k

from just

    ifix :: ((i -> *) -> i -> *) -> i -> *

Having @pat :: k -> k@ we can pack it as

    toPat1 withSpine patN :: ((k -> *) -> *) -> (k -> *) -> *

(where 'withSpine' is constructed automatically from 'k' on the Haskell side) and we can apply
'ifix' to this 1-ary pattern functor and get

    ifix (toPat1 withSpine patN) :: (k -> *) -> *

It only remains to turn something of kind @(k -> *) -> *@ into something of kind @*@, i.e. to define
a type function of kind @((k -> *) -> *) -> k@. But we already have such a function: 'withSpine',
so the final encoding is

    fix = \(patN :: k -> k) -> withSpine (ifix (toPat1 withSpine patN))

The meaning of 'withSpine' here is the same as we've seen before: we use it to pack @n@ type
arguments as a single CPS-encoded spine and pass it to some function.

Summarizing, 'fix' receives an n-ary pattern functor and @n@ type arguments, the pattern functor
gets packed as a 1-ary one, the type arguments get packed into a single CPS-encoded spine and
'ifix' gets applied to the 1-ary pattern functor and the spine.

Read next: Note [Encoded InterList].
-}

{- Note [Encoded InterList]
Let's now look at an example.

Recall that the pattern functor of 'interlist' is

    interlistF =
        \(interlist :: * -> * -> *) (a :: *) (b :: *) ->
            all (r :: *). r -> (a -> b -> interlist b a -> r) -> r

We can apply generic 'fix' (see Note [Generic fix]) to this pattern functor directly:

    fix interlistF :: * -> *

which after eta-expansion and some reductions becomes

    \(a :: *) -> withSpine (ifix (toPat1 withSpine interlistF)) a

(as per Note [Generic fix]) which after some more reductions becomes

    -- Two type arguments that the data type receives and the 'ifix' primitive.
    \(a :: *) (b -> *) -> ifix
        -- The variable responsible for recursion and the variable representing a CPS-encoded spine
        -- of two elements. Note that the kind of the argument that the variable responsible for
        -- recursion receives is the same as the kind of 'spine', i.e. we always instantiate
        -- recursion at some spine.
        (\(rec :: ((* -> * -> *) -> *) -> *) -> \(spine :: (* -> * -> *) -> *) ->
            -- 'spine' unpacks a CPS-encoded spine and passes all its elements to a continuation.
            spine
              -- The 'interlistF' pattern functor given above applied to a function that receives
              -- two type arguments, packs them as a CPS-encoded spine and passes the spine to the
              -- variable responsible for recursion.
              (interlistF (\(a :: *) (b :: *) -> rec (\(dat :: * -> * -> *) -> dat a b)))
        )
        -- The two type arguments packed as a CPS-encoded spine.
        (\(dat :: * -> * -> *) -> dat a b)

We've elaborated the encoding on example, but there is a problem to consider here.
Read next: Note [Denormalization]
-}

255-256: "Then the question is whether it's possible to preserve redexes in user-written types and not to
produce new ones while encoding the types." Why is this question of interest?

Changed this part of the note to

In Plutus Core we have two
modes for type checking:

1. off-chain, type normalization is allowed
2. on-chain, type normalization is not allowed and types must already be normalized

Thus, we do care about whether types are normalized or not. In the compilation pipeline we just
explicitly normalize types whenever normalized types are required, but since this module belongs
to a library it better be general and not rely on particular details of downstream code.

Preserving properties of user-written code is generally a good idea while transforming it,
so we also do not want to remove redexes from user-written code and thus we can't just normalize
everything in sight to overcome the denormalization problem.

Then the question is whether it's possible to preserve redexes in user-written types and not to
produce new ones while encoding the types. And the answer is "yes, but it's too costly".

[effectfully]

Wouldn't it just be the same, only now we pass the two arguments to the saturated form of ifix rather than use function application?

There are two dichotomies here:

1. whether ifix is saturated or not
2. whether ifix is a binder or not

What @psygnisfive proposes is (True, True).
What I propose and what is implemented is (True, False).
What @jmchapman implemented is (False, False) (I think, it's me who proposed to use this in the formalization. Sorry, James!)

So in the implementation ifix is already saturated and we do not use function application there. My comment is about the other dichotomy.

[wadler]

Thanks for the clarification. But I still don't understand the issue. What becomes hard when ifix is a binder that is not hard when ifix is not a binder?

[wadler]

PS: I'm happy with the other responses!

[effectfully]

Thanks for the clarification. But I still don't understand the issue. What becomes hard when ifix is a binder that is not hard when ifix is not a binder?

Now that I think about it, it's not hard, just wordy. Taking my example from the above

treeForestF =
    \(a :: *) (rec :: (* -> * -> *) -> *) (tag :: * -> * -> *) -> all (r :: *).
        tag ((a -> rec forestTag -> r) -> r)
            (r -> (rec treeTag -> rec forestTag -> r) -> r))

tree   = \(a :: *) -> ifix (treeForestF a) treeTag
forest = \(a :: *) -> ifix (treeForestF a) forestTag

in the ifix-as-a-binder setting we can leave treeForestF the same and define tree and forest as

tree   = \(a :: *) -> ifix (rec :: (* -> * -> *) -> *) (tag :: * -> * -> *) (treeForestF a rec tag) treeTag
forest = \(a :: *) -> ifix (rec :: (* -> * -> *) -> *) (tag :: * -> * -> *) (treeForestF a rec tag) forestTag

So in order to be able to compute a pattern functor, you have to bind two type variables using ifix and then pass them to the function returning a pattern functor. Just some inconvenience, but not a big deal. Not as important as my objections from the second message in this thread.

[michaelpj]

It's merged!

[michaelpj]

Okay, let's keep this open until we're done with the spec too.

@psygnisfive did you rename that deliberately?

[wadler]

I'm ok with using ifix in the spec. (But wouldn't kfix make more sense?)

[mchakravarty]

I agree with @effectfully's reasoning.

[effectfully]

I'm ok with using ifix in the spec. (But wouldn't kfix make more sense?)

I think it's my huge mistake that I've been writing ifix :: ((k -> *) -> k -> *) -> k -> *. Perhaps I should go and make it ifix :: ((i -> *) -> i -> *) -> i -> * everywhere.

Here are all the names I'm aware of: ifix (1), hfix(1, 2), fix1 (1), ixfix (1).

kfix can be parsed as "comonadic fixed point".

[michaelpj]

👍 to using an established name. I'm used to ifix now, but hfix also seems to be somewhat common.

I don't think we need to anchor on the usual variable name we use for the kind argument.

[michaelpj]

It looks like we're pretty settled on ifix.