Define `strictify` function at each base type, plus evident property

[jamesmckinna]

For X = ℕ, Bool, Fin n defines:

• strictify : X → X in Data.X.Base
• strictify≗id : strictify x ≡ x in Data.X.Properties

plus:

• specimen use in Relation.Nullary.Decidable.Core cf. discussion on ??? some issue/PR ??? UPDATED: this breaks the build, so clearly there's something not quite right in my analysis!

Issue(s):

• Fairbairn threshold?
• Should there be a parametrised Nullary.Strict record with the above two fields, plus suitable packaging of the above functionality in each case, plus others for List, Maybe, ...? (downstream PR?)

[gallais]

Is this redundant with Function.Strict? I also expect some of these will be optimised away by MAlonzo.

[jamesmckinna]

Is this redundant with Function.Strict?

Ah... my ignorance strikes again

I also expect some of these will be optimised away by MAlonzo.

Indeed.

In any case, the specimen application actually breaks the build, so it's not clear this is even desirable in the first place!

[jamesmckinna]

Is this redundant with Function.Strict?

I've been thinking more about this first point. 'strict' evaluation/function application only forces the argument to be evaluated before entering the body, but that evaluation is still, IIUC, on the normal-order/weak-head strategy, ie we don't achieve the hereditarily strict nature of actual CBV (eg wrt tuples/record values etc.). This is, again IIUC, in harmony with haskell's approach, and seems largely designed to support a definition of seq...?

What's envisaged here is more in line with the idea of 'fully saturated' terms as in Martin-Lof's early writings on type theory, so that strictifying a Boolean really returns a literal value, ditto. for Nat and Fin (so that these are really 'numerals'). of course, one could achieve that via recursive calls to strict application, and perhaps that's a better integrated approach to obtaining such things?

Or have I misunderstood strictness in Agda?

In any case, I think the real issue is to do with 'how strict does strict evaluation of terms of type Dec A need to be, to play well with downstream properties of eg isYes?' and I think I still haven't really appreciated the finer points of constructor-based pattern matching on Dec, even with a 'lazy' pattern, and the even lazier use of the does projection... partly because of (?) the way Reflects is defined... unless I'm still mistaken about that definition in particular, and Agda's evaluation strategies in general ;-)

I also expect some of these will be optimised away by MAlonzo.

That, too, seems fine, even desirable, in a run-time.

[JacquesCarette]

Should an issue be opened to have us agree on 1) the need for this, and 2) if so, its design ?

[jamesmckinna]

No. I think I should close until such time as it bubbles back to the surface in a way which makes sense (to me, and hopefully others ;-))