tag:blogger.com,1999:blog-8068466035875589791.post3970195770082874987..comments2017-05-22T08:50:12.116-07:00Comments on Semantic Domain: Agda is not a purely functional language Neelakantan Krishnaswaminoreply@blogger.comBlogger11125tag:blogger.com,1999:blog-8068466035875589791.post-42170018104595793562017-05-11T17:52:50.700-07:002017-05-11T17:52:50.700-07:00> But as we discussed, the picture is somewhat ...> But as we discussed, the picture is somewhat cloudier than that because alpha equivalence sometimes holds:<br /><br />That example confused me. But in that example proving f, g, and _∧_ equal, you only need eta rules for function types, which Agda supports. Normalization reduces f to 𝜆 x y → f x y and g to 𝜆 x y → g x y (via eta-expansion). Those two functions reduce to 𝜆 x y → x ∧ y by inlining their definitions. _∧_ reduces to 𝜆 x y → x ∧ y by eta-expansion. Since 𝜆 x y → x ∧ y is a normal form, and f, g and _∧_ all reduce to it, they're definitionally equal.<br /><br />Instead, proving equal functions f and g from the blog would require an eta rule on datatypes. Such a rule is false on datatypes with indexes. And it's not enough on structurally recursive functions. Even just eta on sum types is pretty tricky to implement.<br /><br />> The issue with f not being reflexively equal to g seems like an implementation quirk to me.<br /><br />Not quite.<br /><br />> I wonder if they would be equal if expressed via explicit case expressions.<br /><br />You can prove f and g are equal on all inputs (see fx≡gx below), by case analysis on the input, but you can't prove f and g are equal unless you *postulate* extensional equality for functions. This is a consistent postulate, but you can't derive it in Agda or in intensional Martin-Löf type theory.<br /><br />fx≡gx : ∀ x → f x ≡ g x<br />fx≡gx true = refl<br />fx≡gx false = refl<br /><br />> It's really more of an artifact that case-wise pattern match definitions are not done in any principled way in Agda.<br /><br />That seems too harsh. The view from the left explains how you could reduce pattern matching to eliminators, even though that's not implemented.<br /><br />I see that if you reduced to eliminators this particular problem would disappear.<br />Still, the category of sets and functions has extensional equality and Agda and Coq don't—two different stable sorts are extensionally equivalent functions, but not equal.Paolo Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-59765158371026922092016-11-25T15:04:51.090-08:002016-11-25T15:04:51.090-08:00How is declaring a new data type an "effect&q...How is declaring a new data type an "effect"? At best, it's a hidden tag on the type. A piece of data that has no effect on the structure other than distinguishing it from other types which are not tagged the same way.<br /><br />The issue with f not being reflexively equal to g seems like an implementation quirk to me. I wonder if they would be equal if expressed via explicit case expressions. It's really more of an artifact that case-wise pattern match definitions are not done in any principled way in Agda. Which I suppose is a fair criticism.Tac-Ticshttp://www.blogger.com/profile/14070765709653635739noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-70326531952625647482016-08-23T04:44:11.735-07:002016-08-23T04:44:11.735-07:00What about saying to students that Agda is incompl...What about saying to students that Agda is incomplete—f = g is true in at least a model, just not provable. Indeed, postulating extensional equality is known to be consistent (though it does break canonicity of course), hence Jon Sterling (I guess) is right when claiming you can't subvert extensional equality:<br /><br />> Agda may fail to recognize extensional equalities in many cases, but I do not believe it is possible to actually *subvert* extensional equality (i.e. observe that it fails).Paolo Giarrussohttp://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-19294219712021181802016-03-23T11:53:02.252-07:002016-03-23T11:53:02.252-07:00I think this is a laudable but still probably too ...I think this is a laudable but still probably too high standard for what pure functional programming should mean. You seem to be implying that a language is not a pure functional programming language unless all its programs can be treated, using the features of the language, exactly as mathematical functions. So while computationally, programs in Agda behave as pure (total) mathematical functions (their outputs are always defined and always completely determined by their inputs), the reasoning facilities of Agda don't let you equate extensionally equal functions. But I think this is not a fair criticism. You can just as well define a notion of extensional equality, and then functions will be identified if they are input-output equivalent. The fact that the standard propositional equality is not extensional just means that it is not intended for this kind of reasoning. I feel your criticism would be like objecting to the use of propositional equality for reasoning about co-recursively defined values. "Hey, equality is broken for these!" No, we all know you are supposed to use bisimulation for reasoning about streams and such. So I have to say I don't accept your argument that Agda is not a pure functional language. I do appreciate that you raise the point in an interesting way.Aaron Stumphttp://www.blogger.com/profile/07755432667897016469noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-38973057081227661032016-03-23T06:44:41.171-07:002016-03-23T06:44:41.171-07:00I tried to address this issue (that equality is no...I tried to address this issue (that equality is not structural) in the definition of PiSigma which is a partial language with dependent types (hence it is not pure because of non-termination). See http://www.cs.nott.ac.uk/~psztxa/publ/pisigma-new.pdfThorstenhttp://www.blogger.com/profile/11694920694178035992noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-42754207686691584852016-03-23T06:19:52.638-07:002016-03-23T06:19:52.638-07:00Argh, my first work on ML modules was POPL'03,...Argh, my first work on ML modules was POPL'03, not POPL'13. Wishful thinking, old man...Derek Dreyerhttp://www.blogger.com/profile/09408968352547433723noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-74987787177838738702016-03-23T06:19:20.168-07:002016-03-23T06:19:20.168-07:00I would not consider datatype generativity to be a...I would not consider datatype generativity to be a real "effect" in the usual sense. In my first work on ML modules (POPL'13), we called it a "static effect" in the sense that it somehow only takes effect in a kind of static prepass over the program, prior to execution. In particular, you do not want to view datatype generativity as causing a dynamic, computational effect. Zhong Shao did effectively (ho, ho) just this in his ICFP'99 paper, and as a result it meant that in his type system any datatype definitions in the body of a functor forced it to be generative rather than applicative, even though there's no good reason for that. My first real contribution to science, as a matter of fact, was pointing out to my advisors that Shao's treatment of datatype generativity, which matched their own intuitions about generativity as a computational effect, did not in fact match the semantics of OCaml (or Moscow ML). For example, in OCaml, you can have a "generative" definition of datatype T in the body of a functor F, but each application of F to the same argument X will give you the same type F(X).T. As we argue in the F-ing modules paper, this is exactly as it should be because signature ascription (sealing) by itself is not a true effect. A functor should only be treated as generative if the body has true computational effects (whatever those are).<br /><br />Sorry, that was kind of rambling...I'm not sure what is the takeaway for teaching about datatype generativity. Generally, I feel this is a kind of tricky point to explain. There are good "engineering" reasons in practice for datatypes to be opaque rather than transparent, and there are times where this bites you, but it is not so easy to explain the matter directly in terms of effects.Derek Dreyerhttp://www.blogger.com/profile/09408968352547433723noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-15903020337246352872016-03-22T08:20:36.089-07:002016-03-22T08:20:36.089-07:00Excellent point! f ≡ g holds in a univalent type t...Excellent point! f ≡ g holds in a univalent type theory though, so would you say that HoTT is a purely functional language?Vikraman Choudhuryhttp://www.blogger.com/profile/14179847430212299666noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-18566411902285320272016-03-22T03:27:23.881-07:002016-03-22T03:27:23.881-07:00Great post -- I was looking forward to it!
But a...Great post -- I was looking forward to it! <br /><br />But as we discussed, the picture is somewhat cloudier than that because alpha equivalence sometimes holds:<br /><br />_∧_ : Bool → Bool → Bool<br />true ∧ b = b<br />false ∧ b = false<br /><br />f : Bool → Bool → Bool<br />f x y = x ∧ y<br /><br />g : Bool → Bool → Bool<br />g x y = x ∧ y<br /><br />p : f ≡ g<br />p = refl <br /><br />q : f ≡ _∧_<br />q = refl <br /><br />As for interpreting this into the Schanuel topos, it seems to me as an effort to make a bug look like a feature :)<br /><br />drgUnknownhttp://www.blogger.com/profile/14866637943603692944noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-29777120010407960472016-03-21T14:42:14.077-07:002016-03-21T14:42:14.077-07:00One other remark I meant to say is, I am not sure ...One other remark I meant to say is, I am not sure I would agree that this aspect of Agda makes it "impure". Impurity, as far as I (and Longley, and most people) am concerned is when you can define an operation that does not respect equality; Agda may fail to recognize extensional equalities in many cases, but I do not believe it is possible to actually *subvert* extensional equality (i.e. observe that it fails).Unknownhttp://www.blogger.com/profile/04807670051420769844noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-14625426439403497232016-03-21T14:39:11.347-07:002016-03-21T14:39:11.347-07:00Fascinating post! I was going to complain that whi...Fascinating post! I was going to complain that whilst Agda signatures/developments can definitely be seen as formulated internally to the Schanuel topos, Agda *programs* need not be seen in this light, but then I remembered that it is possible to define a fresh datatype inside a where-clause!<br /><br />For what it's worth, in the Red JonPRL proof assistant we have implemented a nominal variant of Computational Type Theory, which can be seen as taking Stuart Allen's meaning explanation for CTT and running it internally inside the Schanuel topos. The correct syntax for this type theory is quite straightforward—we essentially use the abstract binding trees from PFPL, which have nominal characteristics built-in; I've written up the categorical semantics for this, since the precise semantics for the framework were not spelled out in PFPL. As far as the type theory is concerned, do not yet exploit the nominal character of our framework in any significant way, but it will be interesting to see what can be done in the future.<br /><br />-- Jon SterlingUnknownhttp://www.blogger.com/profile/04807670051420769844noreply@blogger.com