Discussion:
Instance resolution question
Add Reply
Apostolis Xekoukoulotakis
2018-03-28 04:39:31 UTC
Reply
Permalink
Raw Message
```
module Test2 where


data A : Set where


CPF : Set
CPF = {{a : A}} → A

postulate
fun : CPF → CPF
e : CPF


bob : CPF
bob {{ctx}} = fun (e {{ctx}})


rob : CPF
rob = fun e

```

I wonder if there is a way to write "rob" instead of "bob".

Keep in mind that the candidates are definitionally equal. (it seems)
Ulf Norell
2018-03-28 05:14:57 UTC
Reply
Permalink
Raw Message
The candidates are not equal. This is what `rob` expands to:

rob : CPF
rob {{ctx}} = fun (λ {{ctx'}} → e)

ctx and ctx' are distinct variables.

/ Ulf

On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
```
module Test2 where
data A : Set where
CPF : Set
CPF = {{a : A}} → A
postulate
fun : CPF → CPF
e : CPF
bob : CPF
bob {{ctx}} = fun (e {{ctx}})
rob : CPF
rob = fun e
```
I wonder if there is a way to write "rob" instead of "bob".
Keep in mind that the candidates are definitionally equal. (it seems)
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-03-28 05:36:22 UTC
Reply
Permalink
Raw Message
https://lists.chalmers.se/pipermail/agda/2017/009802.html

From a previous discussion with Andreas, hidden/instance arguments are
inserted eagerly.
I wonder if I can disable this specifically for "{{ctx}}".
Post by Apostolis Xekoukoulotakis
rob : CPF
rob {{ctx}} = fun (λ {{ctx'}} → e)
ctx and ctx' are distinct variables.
/ Ulf
On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
```
module Test2 where
data A : Set where
CPF : Set
CPF = {{a : A}} → A
postulate
fun : CPF → CPF
e : CPF
bob : CPF
bob {{ctx}} = fun (e {{ctx}})
rob : CPF
rob = fun e
```
I wonder if there is a way to write "rob" instead of "bob".
Keep in mind that the candidates are definitionally equal. (it seems)
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell
2018-03-28 06:30:45 UTC
Reply
Permalink
Raw Message
You can wrap CPF in data type/record:

record CPF : Set where
constructor mkCPF
field unCPF : {{a : A}} → A

postulate
fun : CPF → CPF
e : CPF

rob : CPF
rob = fun e

But note that if it's really `bob` you want, not inserting the {{ctx}} will
give you `cob`, which
is not the same as `bob`:

cob : CPF
cob {{ctx}} = fun (λ {{ctx'}} → e {{ctx'}}) {{ctx}}

/ Ulf

On Wed, Mar 28, 2018 at 7:36 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
https://lists.chalmers.se/pipermail/agda/2017/009802.html
From a previous discussion with Andreas, hidden/instance arguments are
inserted eagerly.
I wonder if I can disable this specifically for "{{ctx}}".
Post by Apostolis Xekoukoulotakis
rob : CPF
rob {{ctx}} = fun (λ {{ctx'}} → e)
ctx and ctx' are distinct variables.
/ Ulf
On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
```
module Test2 where
data A : Set where
CPF : Set
CPF = {{a : A}} → A
postulate
fun : CPF → CPF
e : CPF
bob : CPF
bob {{ctx}} = fun (e {{ctx}})
rob : CPF
rob = fun e
```
I wonder if there is a way to write "rob" instead of "bob".
Keep in mind that the candidates are definitionally equal. (it seems)
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Apostolis Xekoukoulotakis
2018-03-28 07:23:37 UTC
Reply
Permalink
Raw Message
This might work.

(I do want cob and not bob).
Post by Ulf Norell
record CPF : Set where
constructor mkCPF
field unCPF : {{a : A}} → A
postulate
fun : CPF → CPF
e : CPF
rob : CPF
rob = fun e
But note that if it's really `bob` you want, not inserting the {{ctx}}
will give you `cob`, which
cob : CPF
cob {{ctx}} = fun (λ {{ctx'}} → e {{ctx'}}) {{ctx}}
/ Ulf
On Wed, Mar 28, 2018 at 7:36 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
https://lists.chalmers.se/pipermail/agda/2017/009802.html
From a previous discussion with Andreas, hidden/instance arguments are
inserted eagerly.
I wonder if I can disable this specifically for "{{ctx}}".
Post by Apostolis Xekoukoulotakis
rob : CPF
rob {{ctx}} = fun (λ {{ctx'}} → e)
ctx and ctx' are distinct variables.
/ Ulf
On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
Post by Apostolis Xekoukoulotakis
```
module Test2 where
data A : Set where
CPF : Set
CPF = {{a : A}} → A
postulate
fun : CPF → CPF
e : CPF
bob : CPF
bob {{ctx}} = fun (e {{ctx}})
rob : CPF
rob = fun e
```
I wonder if there is a way to write "rob" instead of "bob".
Keep in mind that the candidates are definitionally equal. (it seems)
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...