[Agda] Checking the types of terms

[Guillaume Brunerie]

You could define a function

has-type : (A : Set) (a : A) -> Unit
has-type A a = tt

and then

_ = has-type type1 term1
_ = has-type type2 term2

and so on.
Using the syntax mechanism and an infix symbol, you can even get

_ = term1 :> type1
_ = term2 :> type2

or whatever other symbol you choose.

Guillaume

On Tue, Mar 6, 2018 at 4:27 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 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
>
>
>
> 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
>