[Agda] Checking the types of terms

[Philip Wadler]

Thanks, Guillaume, that solves my problem neatly. 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 19:49, Guillaume Brunerie <guillaume.brunerie at gmail.com>
wrote:

> 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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/17a870ea/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/17a870ea/attachment.ksh>