[Agda] how to evaluate in the current context

[James Wood]

Hi Thorsten,

Just to comment on the bit I think I can comment on,

> P.S. Ok I can say “open Stream public” – but do I want this?

you most probably do want to. My heuristic is that all records should be
opened like this except them acting like typeclasses. More precisely, a
record is acting like a typeclass if its fields are to be seen as ad-hoc
polymorphic values, rather than constituent data of some complex
transient value. Another, seemingly equivalent, condition is whether it
makes sense to work “inside” a specific or general inhabitant.

A good example is to look at monoids vs monoid homomorphisms. If we had
`open Monoid public`, we would have
- Carrier : Monoid → Set
- ε : (M : Monoid) → Carrier M
- _∙_ : (M : Monoid) (x y : Carrier M) → Carrier M
- &c
all in scope (notice how `_∙_` has accidentally become a binary operator
taking three operands). To use these fields, we would always have to
supply the monoid instance `M`. But when we say “suppose M is a monoid”,
we also mean to do `open Monoid M`, so that we don't have to keep giving
the monoid instance. This is what I mean by “working inside an
instance”. Notice that `open Monoid M` is incompatible with `open
Monoid`, as the names would clash.

In contrast, a monoid homomorphism is a single datum, rather than a set
with structure. As such, it doesn't make much sense to work inside a
monoid homomorphism. What we really want to do is be able to deal with
several homomorphisms at once, being perfectly happy with naming the
homomorphism whenever we use any of the data it packs up. In fact, we'd
rather name only the homomorphism, and not precisely which field we're
using, though this is not possible in Agda. While we're naming
inhabitants, it makes sense for all of the eliminators to be visible,
hence `open MonoidHomomorphism public`.

The only other concern is if field names clash with green definitions
from some other module. I think these clashes between eliminators and
definitions should be handled just as clashes between two definitions
would be: at the import site, using qualified imports.

Regards,
James


On 12/05/2020 12:51, Thorsten Altenkirch wrote:
> Hi,
> 
>  
> 
> I have come across this little nuisance when using agda especially when
> doing life hacking in lectures or talks.
> 
>  
> 
> I try to evaluate an expression which depends on opening some modules
> which I have opened in my file but agda is not aware of this. E.g.
> 
>  
> 
> record Stream (A : Set) : Set where
> 
>   constructor _∷_
> 
>   coinductive
> 
>   field
> 
>     hd : A
> 
>     tl : Stream A
> 
>  
> 
> open Stream
> 
>  
> 
> from : ℕ→ Stream ℕ
> 
> hd (from n) = n
> 
> tl (from n) = from (suc n)
> 
>  
> 
> And then I say C-c C-n “hd (from 0)” and agda responds
> 
>  
> 
> 1,1-3
> 
> Not in scope:
> 
>   hd at 1,1-3 (did you mean 'Stream.hd'?)
> 
> when scope checking hd
> 
>  
> 
> Ok I can just introduce a shed
> 
>  
> 
> x = {!!}
> 
>  
> 
> and evaluate inside there but this is a bit clumsy. Isn’t there a better
> way to do this?
> 
>  
> 
> Btw, for the same purposes I’d love to have an agda top-level! And a
> printer that evaluates conductive objects by mapping them to costrings…
> 
>  
> 
> Thorsten
> 
>  
> 
> P.S. Ok I can say “open Stream public” – but do I want this?
> 
>  
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C0aba3584ca574431461508d7f66afebb%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637248811713807387&sdata=bvu3ScVwzFlnypsEQS869A1p1NBOtx5dR5Lqx1kfovE%3D&reserved=0
>