Discussion:
Checking the types of terms
2018-03-06 20:12:06 UTC
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
Larrytheliquid
2018-03-06 20:30:57 UTC
Agda does have underscore definitions, which do not add new identifiers:

\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}
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
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
2018-03-06 21:27:27 UTC
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
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}
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
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
2018-03-06 22:49:16 UTC
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
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
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}
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
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
2018-03-06 22:51:42 UTC
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
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
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
\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}
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
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
2018-03-07 09:01:49 UTC
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
--
Peter Hancock
2018-03-31 12:36:54 UTC
\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.

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