<div dir="ltr">Thanks, Guillaume, that solves my problem neatly. Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 6 March 2018 at 19:49, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You could define a function<br>
<br>
has-type : (A : Set) (a : A) -> Unit<br>
has-type A a = tt<br>
<br>
and then<br>
<br>
_ = has-type type1 term1<br>
_ = has-type type2 term2<br>
<br>
and so on.<br>
Using the syntax mechanism and an infix symbol, you can even get<br>
<br>
_ = term1 :> type1<br>
_ = term2 :> type2<br>
<br>
or whatever other symbol you choose.<br>
<span class="HOEnZb"><font color="#888888"><br>
Guillaume<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Tue, Mar 6, 2018 at 4:27 PM, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> wrote:<br>
> Aha! Good point. I hadn't noticed that underscore lets me achieve my goal.<br>
><br>
> Unfortunately, using underscore takes up twice as many lines. That's not a<br>
> big deal for a single expression, but is a problem if I want to, for<br>
> instance, give a checked signature for every import from a module.<br>
><br>
> Cheers, -- P<br>
><br>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> .   /\ School of Informatics, University of Edinburgh<br>
> .  /  \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
><br>
> On 6 March 2018 at 17:30, Larrytheliquid <<a href="mailto:larrytheliquid@gmail.com">larrytheliquid@gmail.com</a>> wrote:<br>
>><br>
>> Agda does have underscore definitions, which do not add new identifiers:<br>
>><br>
>> \begin{code}<br>
>> _ : type_1<br>
>> _ = term_1<br>
>> ...<br>
>> _ : type_n<br>
>> _ = term_n<br>
>> \end{code}<br>
>><br>
>><br>
>> On Tue, Mar 6, 2018 at 2:12 PM, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> wrote:<br>
>>><br>
>>> A construct like the following would be handy, especially for literate<br>
>>> Agda.<br>
>>> \begin{code}<br>
>>> check<br>
>>>   term_1 : type_1<br>
>>>   ...<br>
>>>   term_n : type_n<br>
>>> \end{code}<br>
>>> Agda checks that each given term has the given type, and typesets the<br>
>>> code, but it introduces no new identifiers and has no effect on the other<br>
>>> code.<br>
>>><br>
>>> Such a construct can allow one to include examples in the text that are<br>
>>> checked by Agda, and hence make the text more reliable. Another use might be<br>
>>> to give types for identifiers imported from elsewhere, making the code<br>
>>> easier to read and allowing Agda to catch any misunderstandings.<br>
>>><br>
>>> Is a feature like this available? Would it be hard to add?<br>
>>><br>
>>> Adding `check` as a keyword would harm backward compatibility, is there<br>
>>> another choice that might be better?<br>
>>><br>
>>> Cheers, -- P<br>
>>><br>
>>> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
>>> .   /\ School of Informatics, University of Edinburgh<br>
>>> .  /  \ and Senior Research Fellow, IOHK<br>
>>> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a><br>
>>><br>
>>> The University of Edinburgh is a charitable body, registered in<br>
>>> Scotland, with registration number SC005336.<br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>><br>
>><br>
>><br>
>><br>
>> --<br>
>> Respectfully,<br>
>> Larry Diehl<br>
><br>
><br>
><br>
> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
><br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
<br>
</div></div></blockquote></div><br></div>