~jonsterling

Cambridge

http://www.jonmsterling.com/

I am an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge in the Department of Computer Science and Technology.

Trackers

~jonsterling/forester

Last active 14 hours ago

#67 Template renders arbitrary content in string-only context 13 hours ago

release-4.2 added by ~jonsterling on ~jonsterling/forester

#70 Allowing macros in more places 13 hours ago

release-4.2 added by ~jonsterling on ~jonsterling/forester

#68 Migrating forester-to-latex to forester 4.2 13 hours ago

release-4.2 added by ~jonsterling on ~jonsterling/forester

#73 Confusing semantics of \let, \def 14 hours ago

needs-design added by ~jonsterling on ~jonsterling/forester

#73 Confusing semantics of \let, \def 14 hours ago

Ticket created by ~jonsterling on ~jonsterling/forester

It occurred to me that in the presence of computational effects (like fluid bindings, shelling out to LaTeX, etc.), the semantics of the current \let construct may be a bit confusing to some users.

Currently, \let is like a private/local version of \def — and so the semantics are "substitutive". A \def or \let expression is substituted during resolution (referred to in the implementation as "expansion") rather than during evaluation. Zooming out, both \def and \let have call-by-name semantics (not wrt. their arguments, but wrt. their context).

Now that we are starting to have more control over evaluation (e.g. via first class functions, lazy arguments, etc.) it might make sense to revisit these semantics. Perhaps, for instance, both \let and \def should have their bodies evaluated eagerly at the definition-site. (When the thing takes arguments, the result would be a closure, so this discussion would only affect nullary definitions.)

I'm curious what people's preferences are, and how we can proceed in a way that either limits breakage or makes the breakage easy to fix.

#72 Call-by-name function arguments a day ago

Comment by ~jonsterling on ~jonsterling/forester

Jon Sterling referenced this ticket in commit 94a179a.

REPORTED RESOLVED CLOSED

#71 Lambda abstraction a day ago

Comment by ~jonsterling on ~jonsterling/forester

Jon Sterling referenced this ticket in commit 94a179a.

REPORTED RESOLVED CLOSED

#72 Call-by-name function arguments a day ago

Comment by ~jonsterling on ~jonsterling/forester

Jon Sterling referenced this ticket in commit 45efd3f.

#71 Lambda abstraction a day ago

Comment by ~jonsterling on ~jonsterling/forester

Jon Sterling referenced this ticket in commit 45efd3f.

#72 Call-by-name function arguments a day ago

Comment by ~jonsterling on ~jonsterling/forester

Jon Sterling referenced this ticket in commit df63757.