[Agda] Checking the types of terms

Peter Hancock hancock at fastmail.fm
Sat Mar 31 14:36:54 CEST 2018


On 06/03/2018 20:30, Larrytheliquid wrote:
> Agda does have underscore definitions, which do not add new identifiers:
> 
> \begin{code}
> _ : type_1
> _ = term_1
> ...
> _ : type_n
> _ = term_n
> \end{code}

Ah! The penny drops! That explains a lot of things I have been reading.


Something I have come to appreciate about Haskell is its nice 
use of underscores, so you can read 

k x _ = x,

without having to search through some enormous right-hand-side to see if some 
spuriously-invented name occurs there. Three cheers for that. 

Agda seems to take this further, from argument lists to the whole name-space.
It seems a very nice feature.  Remembering or thinking up names for things 
that are never going to be referenced is not fun. It is hard enough when they
are referenced. 

Hank





More information about the Agda mailing list