search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Document required Agda version #2

Closed eternaleye closed 7 years ago

eternaleye commented 7 years ago

I'm attempting to build the project, but am encountering syntax errors both with Agda 2.5.2 and git HEAD (https://github.com/agda/agda/commit/01798f3e0bbd6eec2346b83388f54d78432f550f). Is there any chance that the Agda version needed could be noted somewhere, even if just as a comment in the Makefile?

vikraman commented 7 years ago

I'm happy that someone is trying to build our paper!

The Makefile builds fractypes.pdf which was written before agda 2.5.2 was released, so I think it should build correctly with agda 2.5.1. The other files since then should work with version 2.5.2.

eternaleye commented 7 years ago

Hm, I think there may be a bit more than that compatibility wise- when I try to build it, the errors I'm getting are things like

agda --allow-unsolved-metas --latex -i . --latex-dir=. groupoid.lagda
/home/Alex.Elsayed/2DTypes/groupoid.lagda:469,27-27
/home/Alex.Elsayed/2DTypes/groupoid.lagda:469,27: Parse error
{<ERROR>
%     Obj = Iter p
%  ; _⇒_ = ...
make: *** [Makefile:24: groupoid.tex] Error 1

And if I remove the offending code section, it moves on to complain about

agda --allow-unsolved-metas --latex -i . --latex-dir=. groupoid.lagda
/home/Alex.Elsayed/2DTypes/groupoid.lagda:716,3-3
/home/Alex.Elsayed/2DTypes/groupoid.lagda:716,3: Parse error
data<ERROR>
 FT/ : Set where
%   ⇑    : FT...
make: *** [Makefile:24: groupoid.tex] Error 1

I'll certainly try 2.5.1, though!

Anyway, I'm glad I found this paper! A couple years back I I got interested in reversible computing, but didn't find anything really striking until I encountered "Information Effects" (and then "The Computational Content of Isomorphisms", followed by the rest of the \Pi saga).

I've been avidly following anything derived from it ever since; it gives me the same feeling that there's a powerful unifying framework present as when I was first learning about the Lambda calculus and the Curry-Howard isomorphism.

One thing that tickled my fancy with fractional types, in fact, is that with isorecursive types you can describe infinite continued fractions... which look an awful lot like infinite session types, such as \mu x. 1 + 1/x being both "the session type of dynamically-terminating ping-pong benchmarks" and "the golden ratio."

Of course, isorecursive types in \Pi grant Turing-completeness, but that seems to feed back nicely into Sabry's observations about quantum mechanics and infinitely-sized reals.

JacquesCarette commented 7 years ago

If you're into the \Pi saga, have you read "Computing with semirings and weak rig groupoids"? Paper at https://www.cs.indiana.edu/~sabry/papers/weak-rig-groupoid.pdf, Agda repo at https://github.com/JacquesCarette/pi-dual/tree/master/Univalence.

eternaleye commented 7 years ago

Indeed I have! We actually talked over email, at one point :P

JacquesCarette commented 7 years ago

Indeed - I just didn't immediately recognize the handle. But I've found the conversation now.

eternaleye commented 7 years ago

Well, Agda 2.5.1.2 gets me to the point of LaTeX, but something seems to be making pdflatex very unhappy around line 78 of opsem.lagda:

Runaway argument?
\ignorespaces  mutual 𝓐𝓹 : {τ₁ τ₂ : U} → (τ₁ ⟷ τ�\ETC.
! Paragraph ended before \PT@scantoend was complete.
vikraman commented 7 years ago

I setup travis-ci to automatically build a draft and publish it to releases and I'll try to maintain it for future papers.