[Agda] Checking the types of terms

[Philip Wadler]

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/

[Larrytheliquid]

Agda does have underscore definitions, which do not add new identifiers:

\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}

Post by Philip Wadler
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
https://lists.chalmers.se/mailman/listinfo/agda

[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/

Post by Philip Wadler
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}

Post by Philip Wadler
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
https://lists.chalmers.se/mailman/listinfo/agda

--
Respectfully,
Larry Diehl

[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

Post by 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/

Post by Philip Wadler
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}

Post by Philip Wadler
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
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
https://lists.chalmers.se/mailman/listinfo/agda

[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/

Post by 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

Post by Philip Wadler
Aha! Good point. I hadn't noticed that underscore lets me achieve my

goal.

Post by Philip Wadler
Unfortunately, using underscore takes up twice as many lines. That's not

a

Post by Philip Wadler
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/

Post by Philip Wadler
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}

Post by Philip Wadler
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

Post by Philip Wadler

Post by Philip Wadler

Post by Philip Wadler
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

Post by Philip Wadler

Post by Philip Wadler

Post by Philip Wadler
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
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
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Guillaume Brunerie
Using the syntax mechanism and an infix symbol, you can even get
_ = term1 :> type1
_ = term2 :> type2
or whatever other symbol you choose.

And you can hide parts of the code:

\begin{code}[hide]
_ =
\end{code}
\begin{code}
term1 :> type1
\end{code}

(This is assuming that you are using the development version of Agda.
Agda 2.5.3 provides a different syntax for hiding code, see
http://agda.readthedocs.io/en/v2.5.3/tools/generating-latex.html#features.)

[Peter Hancock]

Post by Philip Wadler
\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