CohenCyril pushed 1 commit to branch parameters.

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

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.

CohenCyril pushed 1 commit to branch parameters.

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

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.

```
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).
```

@Enrico Tassi am I taking this too far?

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)

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

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

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.

no, subject first. Also `map {map {map L f} g} h} L1`

does not seem that bad

If you want the other way, you can `map L (x\ map x F) L1`

which is not that bad ither

If I had time I'd probably add something like `map L (map ? F) L1`

(Scala like) to denote the latter

But You can also add a clause `^~`

and do `^~ map F`

and mark ^~ as infix

`map ^~ F`

Why subject first?

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

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**

(I can be opinonated too :wink:)

Partial application is bullshit

Enrico Tassi said:

Partial application is bullshit

hum, no?

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

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

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

(and remap yours `doneleft.`

)

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

all the catamorphisms & co

ok, actually, my example was a bit more complicated than just `map`

of itself but you get the spirit

write your combinators in `fun.`

, I'm serious.

then I'll see what it looks like.

I would like to write `w-params.map (map triple_1) X Y`

instead of `w-params.map X (x\ map x triple_1) Y`

for example.

cf math-comp/hierarchy-builder#610df064862d7849b51ddc1a3796a43bb8abc517

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

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

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

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

so `list`

or `fun`

as a namespace... BTW I cannot find the source file for `std`

...

(is it generated?)

https://github.com/LPCIC/elpi/blob/master/src/builtin_stdlib.elpi

I prefer `list`

(for list functions)

this file is then used to produce builtins.elpi

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

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

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

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

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

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

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

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

you have so many "opinions"! :kitten:

Maybe I adding the `list`

name space could be this minor "bugfix" :laughing:

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

@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`

?

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.

You can `(the-type A B :- !) => G`

if you want to mask

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

So I suggest you add the `!`

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