w-param refactoring · Hierarchy Builder devs & users

Stream: Hierarchy Builder devs & users

Topic: w-param refactoring

HB Github Bot (May 13 2020 at 01:49):

CohenCyril pushed 1 commit to branch parameters.

pinning a coq-elpi revision compatible with elpi-1.10.2 (2e82239)

HB Github Bot (May 13 2020 at 01:49):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.
The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

HB Github Bot (May 13 2020 at 09:56):

CohenCyril pushed 1 commit to branch parameters.

refactor factories-provide with list-w-params.flatten-map (c91ff5e)

HB Github Bot (May 13 2020 at 09:56):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.
The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

Cyril Cohen (May 13 2020 at 12:49):

kind w-params (type -> type) -> type -> type.
type w-params.cons name -> term -> (term -> w-params C A) -> w-params C A.
type w-params.nil name -> term -> (term -> C (w-args A)) -> w-params C A.

does not work but

kind w-params type -> type -> type.
type w-params.cons name -> term -> (term -> w-params C A) -> w-params C A.
type w-params.nil name -> term -> (term -> C (w-args A)) -> w-params C A.

does, and apparently I can do:

typeabbrev (list-w-params A) (w-params list A).

but not

typeabbrev (one-w-params A) (w-params (x\x) A).

Cyril Cohen (May 13 2020 at 12:50):

@Enrico Tassi am I taking this too far?

Enrico Tassi (May 13 2020 at 13:23):

I think that the standard type system for LP does not accept the Haskellian kind of your first attempt, and the second attempt works simply because the type checker messes up forall/exist quantifications... The last example probably fails because the type checker does not even have "lambda abstraction" in the syntax of types (see https://github.com/LPCIC/elpi/blob/42d7b046c74d230288a3c40a9410d697f601fb56/src/elpi-checker.elpi#L9)

Enrico Tassi (May 13 2020 at 13:27):

To be honest, the type checker of elpi is too ugly for that. It is too ugly in many ways and I've never had the time to make it better. I think it is more safe to have the 2 data types and leave the first version in a comment, with a TODO and possibly an issue on elpi asking for type quantification on type-functions

Cyril Cohen (May 18 2020 at 10:34):

@Enrico Tassi while your at it, would it be possible to swap the arguments of std.map, std.filter and the like, to put functions first, it makes composition much easier this way... (e.g. map (map f) makes sense...

HB Github Bot (May 18 2020 at 11:01):

CohenCyril updated PR #65 [feature] parameters in structures from parameters to master:

HB.mixin Record (P1 : T1) ... (A : Type) foo of f1 P1 A & .. & f2 P1 (P1 * P2) A := { ... }.
The key is to represent the dispatching a factory does of its parameters to the underlying mixins.
Here for example here foo P1 .. passes P1 to f1 and P1, P1 * P2 to f2.
A dispatching is an arbitrary function from parameters to a list of parameters.

Enrico Tassi (May 18 2020 at 12:02):

no, subject first. Also map {map {map L f} g} h} L1 does not seem that bad

Enrico Tassi (May 18 2020 at 12:04):

If you want the other way, you can map L (x\ map x F) L1 which is not that bad ither

Enrico Tassi (May 18 2020 at 12:05):

If I had time I'd probably add something like map L (map ? F) L1 (Scala like) to denote the latter

Enrico Tassi (May 18 2020 at 12:06):

But You can also add a clause ^~ and do ^~ map F and mark ^~ as infix

Enrico Tassi (May 18 2020 at 12:06):

map ^~ F

Cyril Cohen (May 18 2020 at 14:06):

Why subject first?

Enrico Tassi (May 18 2020 at 14:10):

Because I say so ;-) You are entering a very opinionated room ...
I dislike the way map is done in OCaml, when you first read how and then what. The new |> thing is just an admission of guilt

Cyril Cohen (May 18 2020 at 14:16):

Arg, when you read f x you still read f before x... so if you start applying on the right, at least be consistent and keep applying on the right so that everything is on the same side as in map f x ...
Writing map x f is a crazy mix. If you really want to read the operation after the subject, use postfix application and then I am all in for x f map... but having half of the things on the right and half on the left drives me crazy and breaks compositionality

Cyril Cohen (May 18 2020 at 14:17):

(I can be opinonated too :wink:)

Enrico Tassi (May 18 2020 at 14:19):

Partial application is bullshit

Cyril Cohen (May 18 2020 at 14:20):

Enrico Tassi said:

Partial application is bullshit

hum, no?

Cyril Cohen (May 18 2020 at 14:23):

come on... partial applications and monads are on a boat, monads fall overboard... who stays???

Cyril Cohen (May 18 2020 at 14:25):

so please allow indexing at any position and let's swap the map? :cat:

Cyril Cohen (May 18 2020 at 14:26):

or I will write a library with the right positions in the namespace doneright.

Cyril Cohen (May 18 2020 at 14:26):

(and remap yours doneleft.)

Enrico Tassi (May 18 2020 at 14:27):

elpi now can index at any position, but I don't like map that way, it not common to pass around (map f) to lift to list another mapping
I'm perfectly fine with a library in the namespace fun. that has all the applicative-functoriality you like

Enrico Tassi (May 18 2020 at 14:27):

all the catamorphisms & co

Cyril Cohen (May 18 2020 at 14:28):

ok, actually, my example was a bit more complicated than just map of itself but you get the spirit

Enrico Tassi (May 18 2020 at 14:29):

write your combinators in fun., I'm serious.

Enrico Tassi (May 18 2020 at 14:29):

then I'll see what it looks like.

Cyril Cohen (May 18 2020 at 14:31):

I would like to write w-params.map (map triple_1) X Y instead of w-params.map X (x\ map x triple_1) Yfor example.

Cyril Cohen (May 18 2020 at 14:38):

cf math-comp/hierarchy-builder#610df064862d7849b51ddc1a3796a43bb8abc517

Enrico Tassi (May 18 2020 at 14:46):

what about w-params.map X (list.map triple_1) Y

Enrico Tassi (May 18 2020 at 14:47):

or even w-params.map (list.map triple_1) X Y

Enrico Tassi (May 18 2020 at 14:50):

but you see that the subject has gone in another room, which does not improve readability, IMO.

Cyril Cohen (May 18 2020 at 14:56):

Enrico Tassi said:

or even w-params.map (list.map triple_1) X Y

Sure, that's my preference... I prefer this to

or even w-params.map X (x \ std.map x triple_1) Y

where the subject is in between two functions and the functional argument is less readable

Cyril Cohen (May 18 2020 at 14:56):

so list or fun as a namespace... BTW I cannot find the source file for std...

Cyril Cohen (May 18 2020 at 14:56):

(is it generated?)

Enrico Tassi (May 18 2020 at 15:10):

https://github.com/LPCIC/elpi/blob/master/src/builtin_stdlib.elpi
I prefer list (for list functions)

Enrico Tassi (May 18 2020 at 15:10):

this file is then used to produce builtins.elpi

Enrico Tassi (May 18 2020 at 15:14):

You can do a file builtin_list.elpi then do as for the other file

Enrico Tassi (May 18 2020 at 15:16):

there is a rule in the dune file and a mention in builtin.ml

Enrico Tassi (May 19 2020 at 13:23):

I made a new big push in coq-elpi/master and hierarcy-builder/coq-elpi-1.4, I think you should rebase

Enrico Tassi (May 19 2020 at 13:24):

I've also fixed the "cannot spill" without a location error, and the unclickable parse error thing (this last is in elpi :-/)

Enrico Tassi (May 19 2020 at 13:24):

To me the head of coq-elpi/master is 99% coq-elpi 1.4

Cyril Cohen (May 19 2020 at 13:44):

and there will be a elpi-1.11.3 to fix the unclickable parse error?

Enrico Tassi (May 19 2020 at 13:57):

hum... if you find another minor bug I'll make a minor release ;-)

Enrico Tassi (May 19 2020 at 13:58):

making a release for 1 commit like that... dunno

Cyril Cohen (May 19 2020 at 14:01):

you have so many "opinions"! :kitten:

Cyril Cohen (May 19 2020 at 14:10):

Maybe I adding the list name space could be this minor "bugfix" :laughing:

Enrico Tassi (May 19 2020 at 14:15):

no, that would not be minor... although very welcome.

Cyril Cohen (May 19 2020 at 14:55):

@Enrico Tassi (is it true and) can I rely on the fact that the-type P1 X1 => the-type P2 X2 => the-type P3 X3 yields P3 = P2 and X3 = X2?

Enrico Tassi (May 19 2020 at 14:56):

it yields both, the only you like first, the other as a second result. You can assume that in P => G, P has the highest precedence.

Enrico Tassi (May 19 2020 at 14:57):

You can (the-type A B :- !) => G if you want to mask

Enrico Tassi (May 19 2020 at 14:58):

it looks anyway weird to have a predicate called the-something if there are 2 of that kind ;-)

Enrico Tassi (May 19 2020 at 14:59):

So I suggest you add the !

Cyril Cohen (May 19 2020 at 16:42):

Yeah, that's bothering meee... But in case of nested calls of w-params.then I'm f*... So I will parametrize over the database!!!!

Last updated: May 28 2023 at 18:29 UTC