Stream: Hierarchy Builder devs & users

Topic: w-param refactoring


view this post on Zulip HB Github Bot (May 13 2020 at 01:49):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip 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.

view this post on Zulip HB Github Bot (May 13 2020 at 09:56):

CohenCyril pushed 1 commit to branch parameters.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Cyril Cohen (May 13 2020 at 12:50):

@Enrico Tassi am I taking this too far?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 18 2020 at 12:06):

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

view this post on Zulip Enrico Tassi (May 18 2020 at 12:06):

map ^~ F

view this post on Zulip Cyril Cohen (May 18 2020 at 14:06):

Why subject first?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:17):

(I can be opinonated too :wink:)

view this post on Zulip Enrico Tassi (May 18 2020 at 14:19):

Partial application is bullshit

view this post on Zulip Cyril Cohen (May 18 2020 at 14:20):

Enrico Tassi said:

Partial application is bullshit

hum, no?

view this post on Zulip Cyril Cohen (May 18 2020 at 14:23):

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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:25):

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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:26):

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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:26):

(and remap yours doneleft.)

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 18 2020 at 14:27):

all the catamorphisms & co

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 18 2020 at 14:29):

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

view this post on Zulip Enrico Tassi (May 18 2020 at 14:29):

then I'll see what it looks like.

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (May 18 2020 at 14:38):

cf math-comp/hierarchy-builder#610df064862d7849b51ddc1a3796a43bb8abc517

view this post on Zulip Enrico Tassi (May 18 2020 at 14:46):

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

view this post on Zulip Enrico Tassi (May 18 2020 at 14:47):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:56):

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

view this post on Zulip Cyril Cohen (May 18 2020 at 14:56):

(is it generated?)

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (May 18 2020 at 15:10):

this file is then used to produce builtins.elpi

view this post on Zulip Enrico Tassi (May 18 2020 at 15:14):

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

view this post on Zulip Enrico Tassi (May 18 2020 at 15:16):

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

view this post on Zulip 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

view this post on Zulip 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 :-/)

view this post on Zulip Enrico Tassi (May 19 2020 at 13:24):

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

view this post on Zulip Cyril Cohen (May 19 2020 at 13:44):

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

view this post on Zulip Enrico Tassi (May 19 2020 at 13:57):

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

view this post on Zulip Enrico Tassi (May 19 2020 at 13:58):

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

view this post on Zulip Cyril Cohen (May 19 2020 at 14:01):

you have so many "opinions"! :kitten:

view this post on Zulip Cyril Cohen (May 19 2020 at 14:10):

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

view this post on Zulip Enrico Tassi (May 19 2020 at 14:15):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 19 2020 at 14:57):

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

view this post on Zulip 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 ;-)

view this post on Zulip Enrico Tassi (May 19 2020 at 14:59):

So I suggest you add the !

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC