[Agda] Checking the types of terms

[Philip Wadler]

Aha! Good point. I hadn't noticed that underscore lets me achieve my goal.

Unfortunately, using underscore takes up twice as many lines. That's not a
big deal for a single expression, but is a problem if I want to, for
instance, give a checked signature for every import from a module.

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 6 March 2018 at 17:30, Larrytheliquid <larrytheliquid at gmail.com> wrote:

> Agda does have underscore definitions, which do not add new identifiers:
>
> \begin{code}
> _ : type_1
> _ = term_1
> ...
> _ : type_n
> _ = term_n
> \end{code}
>
>
> On Tue, Mar 6, 2018 at 2:12 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>
>> A construct like the following would be handy, especially for literate
>> Agda.
>> \begin{code}
>> check
>>   term_1 : type_1
>>   ...
>>   term_n : type_n
>> \end{code}
>> Agda checks that each given term has the given type, and typesets the
>> code, but it introduces no new identifiers and has no effect on the other
>> code.
>>
>> Such a construct can allow one to include examples in the text that are
>> checked by Agda, and hence make the text more reliable. Another use might
>> be to give types for identifiers imported from elsewhere, making the code
>> easier to read and allowing Agda to catch any misunderstandings.
>>
>> Is a feature like this available? Would it be hard to add?
>>
>> Adding `check` as a keyword would harm backward compatibility, is there
>> another choice that might be better?
>>
>> Cheers, -- P
>>
>> .   \ Philip Wadler, Professor of Theoretical Computer Science,
>> .   /\ School of Informatics, University of Edinburgh
>> .  /  \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
>
> --
> Respectfully,
> Larry Diehl
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/8496fb35/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/8496fb35/attachment.ksh>