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!

[JacquesCarette]

I think strictify and its defining property, i.e. strictify≗id should be a proper structure that one can instantiate, instead of being ad hoc name sharing.

It might even deserve to be a typeclass?

[JacquesCarette]

Oh my. This is the code that I consider amongst the most evil! Can't it at least be written

strictify true = true
strictify false = false

?

[jamesmckinna]

Agree that, in novice programmers, that one-line expression is truly evil.

But it nevertheless is precisely equivalent to your definition (up to reduction/strictness behaviour), for the (additional) cost of a (generatively distinct) function definition.

Cf. defining _++_ directly, or as an instance of foldr?

[JacquesCarette]

I sure hope those definitions are precisely equivalent! strictify is weird, I don't really mind if it has a cost.

I personally think the computational _++_ should be defined in terms of foldr.

[jamesmckinna]

Well, as with my comments below, I believe on my understanding of Agda's evaluation strategy that they are reduction-behaviour equivalent, in that they are each

• blocked, neutral terms, if the Bool scrutinee is unevaluated/neutral
• the relevant literal value, depending on the value of the scrutinee

I've wondered if, as in a separate issue/PR, we considered systematically adding the dependent/non-dependent eliminators for Data.X, the 'evil' arises because of our habit of not seeing if_then_else as 'merely' the non-dependent eliminator for Bool? (The separate evil of novice programmers writing if b then true else false in a strict language is another matter...)

[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.