<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi Oscar,</div><div><br></div><div>I may not be the best person to answer some of your questions but I just felt like having a go at you little quiz...</div><div><br><blockquote type="cite"><div>I've got some newbie questions after reading (and writing the code in)<br>Dependently Typed Programming in Agda.<br><br>1. Is it possible to use "record syntax" (names parameters) for<br>functions even when the arguments aren't implicit? I.e. can I<br>construct named explicit arguments?<br>I would like to be able do something like:<br><blockquote type="cite">foo : (x : Nat) -> Nat<br></blockquote><blockquote type="cite">answer = foo { x = 42 }<br></blockquote><blockquote type="cite">answer2 = foo 42<br></blockquote></div></blockquote><div><br></div><div>I think explicit parameters are only positional.</div><br><blockquote type="cite"><div><br>2. What does it mean when a function declaration got a signature like<br><blockquote type="cite">isTrue : Bool → Set<br></blockquote></div></blockquote><div><br></div><div>It eats booleans and shits sets.</div><br><blockquote type="cite"><div>Is isTrue a decomposer? </div></blockquote><div><br></div><div>What is a decomposer?</div><br><blockquote type="cite"><div>Is the type checker aware that True and False</div></blockquote><blockquote type="cite"><div>are the only valid types from isTrue?<br></div></blockquote><div><br></div><div>Nope.</div><br><blockquote type="cite"><div>Why is<br><blockquote type="cite">isTrue : Bool -> Set<br></blockquote><blockquote type="cite">isTrue true = True<br></blockquote><blockquote type="cite">isTrue false = False<br></blockquote>valid but not the reverse, i.e.<br><blockquote type="cite">isBool : Set -> Bool<br></blockquote><blockquote type="cite">isBool True = true<br></blockquote><blockquote type="cite">isBool False = false<br></blockquote></div></blockquote><div><br></div><div>You can't match against a set, Agda just thinks that True and False a variables. The Haskell convention that capital letters indicate constructors does not apply to Agda.</div><br><blockquote type="cite"><div>isn't? Agda will complain about:<br>"Unreachable clause<br>when checking the definition of getBool"<br>regarding the last case (isBool False). It's however accepting the<br>code if I remove the last isBool-pattern (False = false).<br></div></blockquote><div><br></div><div>Sure, it's just a catch all.</div><br><blockquote type="cite"><div>It seems to accept<br><blockquote type="cite">data Foo : Set where<br></blockquote><blockquote type="cite">checkIsTrue : (x : Bool) → (isTrue x) → Bool<br></blockquote><blockquote type="cite">checkIsTrue true True = false<br></blockquote><blockquote type="cite">checkIsTrue false Foo = true<br></blockquote>as complete but I think (and Agda can also accept) the last pattern<br>match should be<br><blockquote type="cite">checkIsTrue false False = true<br></blockquote>since "false Foo" cannot happen. I'm clearly misunderstanding<br>something here since I thought that (isTrue x) should make sure that<br>the second argument is a valid value given a first value (i.e.<br>"checkIsTrue true True" should be a valid pattern while "checkIsTrue<br>true False" or "checkIsTrue true Foo" shouldn't).<br></div></blockquote><div><br></div>You are on the wrong track here.<br><blockquote type="cite"><div><br>3. Is there any interpreter like ghci for Agda?<br></div></blockquote><div><br></div><div>What is wrong with C-c C-n?</div><br><blockquote type="cite"><div>4. How can I make C-x C-l run faster (it's usually freezing emacs for<br>5-15 seconds)? </div></blockquote><div><br></div><div>Good question.</div><br><blockquote type="cite"><div>It seems to spend a lot of time in ghc. I suspect it's<br>recompiling code from the Agda standard library every time.<br></div></blockquote><div><br></div><div>I think it is just loading the library.</div><div><br></div><blockquote type="cite"><div><br>5. Which keywords got fancy utf-8 alternatives? I've found forall (∀)<br>and -> (→) so far. Any I've missed?<br><br>6. Is there any tool like Haddock for generating documentation?<br></div></blockquote><div><br></div><div>No, but you can generate html from Agda code with links to the definitions. It's a flag to the agda command line interface (--html).</div><br><blockquote type="cite"><div><br>7. Which font do you use in Emacs (Mac OS X)? Sometimes squares show<br>up (in the standard library) where it probably should be some utf-8<br>symbol.<br></div></blockquote><div><br></div><div>I don't have this problem. I am using Aquamacs.</div><br><blockquote type="cite"><div><br>8. How do you use {! !}? After running C-x C-l I receive suggestions<br>but can I somehow automatically insert them?<br><br></div></blockquote><div><br></div><div>?</div><br><blockquote type="cite"><div>9. What is the value from an absurd pattern? ()? If it's (): what does<br>it mean? Something like Haskell's undefined?<br></div></blockquote><div><br></div><div>No, it is an impossible pattern. But if one would just leave out the line this would make the job harder for the pattern completeness checker.</div><br><blockquote type="cite"><div><br>10. Regarding absurd patterns (p. 9). I don't understand why Fin zero<br>is a valid type. Shouldn't all FinS begin with Fin (suc ...) and isn't<br>dependent typing about enforcing this?<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>Fin zero is a fine type, it is just empty.<br><br><blockquote type="cite"><div>11. Is there anything like Haskell type classes in Agda? I've read<br>that there aren't but <a href="http://types2004.lri.fr/SLIDES/coquand.pdf">http://types2004.lri.fr/SLIDES/coquand.pdf</a> seems<br>to indicate there are. Or are the slides just a proposal for new<br>functionality? If there are no type classes: can they be simulated<br>somehow using some Agda technique?<br></div></blockquote><div><br></div><div>This may be outdated.</div><div><br></div><div>Otherwise it is a good question. Many uses of type classes are covered by dependent types, but not all.</div><br><blockquote type="cite"><div><br>12. Is there any up-to-date tutorial/documentation for Agda?<br>"Dependently Typed Programming in Agda" was excellent as an<br>introduction but a bit dated (e.g. standard lib not the same).<br></div></blockquote><div><br></div><div>I am using Agda in a 3rd year course in Nottingham</div><div><a href="http://www.cs.nott.ac.uk/~txa/g52ifr/">http://www.cs.nott.ac.uk/~txa/g52ifr/</a></div><div>but I am not sure that's what you are looking for.</div><br><blockquote type="cite"><div><br>13. What are Sigma and Pi that are mentioned sometimes? Googling them<br>is a bit hard... .<br></div></blockquote><div><br></div><div>Pi types are dependent function types (x : A) → B x which were traditionally written as Π x : A . B x.</div><div>Sigma types are dependent product types (import Data.Product), in Agda Σ A (λ x → B x), traditionally</div><div>Σ x : A. B x.</div><div><br></div><div>As one rarely needs products in Haskell, one rarely uses Sigma types in Agda.</div><br><blockquote type="cite"><div><br>14. How do I construct integers (not Nat) and floats in Agda?<br>I understand that I can do something like<br><blockquote type="cite">answer : ℕ<br></blockquote><blockquote type="cite">answer = 42<br></blockquote>but that 42 won't be the same as an Haskell 42 right (i.e. Integer)?<br></div></blockquote><div><br></div><div>I think there is library for integers but these are not machine integers.</div><br><blockquote type="cite"><div>How can I interface between Haskell primitives (Integer, Float) and<br>Agda primitives? All info I find is regarding Char and String. It is<br>somehow possible to convert an Haskell Integer into an Agda ℕ?<br></div></blockquote><div><br></div><div>Somebody else better answers this.</div><br><blockquote type="cite"><div><br>15. I cannot get the function "find" on p. 25 (Dependently Typed<br>Programming in Agda) to compile.<br>I get the error<br><blockquote type="cite">F (p x) !=< T (not (p (_226 p xs npxs x prf))) of type Set<br></blockquote><blockquote type="cite">when checking that the expression falseIsFalse prf has type<br></blockquote><blockquote type="cite">T (not (p (_226 p xs npxs x prf)))<br></blockquote>regarding "falseIsFalse" on the last line in the function and I'm not<br>knowledgeable enough in Agda to understand that error message.<br>Not that it matters much, just thought someone (Ulf Norell?) might want to know.<br></div></blockquote><div><br></div><div>I better leave this to Ulf. Certainly Agda is evolving quicker than its documentation....</div><br><blockquote type="cite"><div><br>16. Why is False defined as<br><blockquote type="cite">data False : Set where<br></blockquote></div></blockquote><div><br></div><div>False = the empty set is the set with no constructors.</div><br><blockquote type="cite"><div>while True is defined as<br><blockquote type="cite">record True : Set where<br></blockquote>and why aren't both using the same sort of definition (data or record)?<br></div></blockquote><div><br></div><div>True is the record with no fields, i.e. a one element set.</div><div><br></div><div>Using records to define True has the advantage that there is eta equality for records and hence elements of True can always be completed by the type checker.</div><div><br></div><div>There is no way to define False using records.</div><br><blockquote type="cite"><div><br>17. Why is [_] (in Data.List) defined as<br><blockquote type="cite">forall {a} {A : Set a} -> A -> List A<br></blockquote>and not simply<br><blockquote type="cite">{A : Set} -> A -> List A<br></blockquote>and what does "Set a" mean? It seems to have something to do with<br>--universe-polymophism... .<br><br>18. Why is the type declaration for apply (in the paper/tutorial by Ulf Norell):<br><blockquote type="cite">(A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a<br></blockquote>and not<br><blockquote type="cite">(A : Set)(B : A -> Set) -> (A -> B A) -> A -> B A<br></blockquote></div></blockquote><div><br></div><div>Oops, this doesn't type check, B eats As not sets. </div><br><blockquote type="cite"><div>or even</div></blockquote><blockquote type="cite"><div><blockquote type="cite">{A B : Set} -> (A -> B) -> A -> B<br></blockquote>analogous to the declaration for map?<br></div></blockquote><div><br></div><div>This is the non-dependent apply. Btw there is also a dependent map. Another story.</div><br><blockquote type="cite"><div><br>19. What is it called when you got a constructor in the declaration, e.g. in Vec<br><blockquote type="cite">_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)<br></blockquote>where "suc" is used. What is "suc" (or similar constructors) called<br>when used in declarations? </div></blockquote><div><br></div><div>Why should it be called something special?</div><br><blockquote type="cite"><div>Are there any restrictions on what kind of<br>constructors that are allowed? </div></blockquote><div><br></div><div>Who told you that only constructors are allowed?</div><br><blockquote type="cite"><div>n is a value so obviously values are<br>permitted as well. Are there any restrictions of which values can be<br>used or can arbitrary functions be used and would thus something like<br><blockquote type="cite">listToVec : {A : Set} -> (x: List A) -> Vec A (length x)<br></blockquote><blockquote type="cite">listToVec [] = []<br></blockquote><blockquote type="cite">listToVec x :: xs = x :: (listToVec xs)<br></blockquote>be allowed?<br><br></div></blockquote><div><br></div><div>Yes, just try it.</div><br><blockquote type="cite"><div>20. In vmap₃ (p 9) why isn't nil dotted, i.e. replace<br><blockquote type="cite">vmap₃ zero f nil = nil<br></blockquote>with<br><blockquote type="cite">vmap₃ zero f .nil = nil<br></blockquote>since the only valid value for the third argument is nil?<br></div></blockquote><div><br></div><div>You only dot if you repeat variables.</div><br><blockquote type="cite"><div>21. What is the difference between parameters and indices of a<br>datatype (except syntactically)? Is there something you can do with<br>one that you cannot do with the other? When should I preferre one over<br>the other?<br></div></blockquote><div><br></div><div>If you can use parameters this is usually better (certainly saves quantifying over them in the constructor type).</div><div>But if you use the type at different instance this is not possible.</div><div><br></div><div>Parameters also behave differently wrt size (set levels) but this is maybe a more advanced topic.</div><br><blockquote type="cite"><div><br>22. There seems to be some functions that end with "Set" and some that<br>begin with "Set", e.g.<br><blockquote type="cite">_==_ : {A : Set} → A → A → Set<br></blockquote><blockquote type="cite">isTrue : Bool -> Set<br></blockquote>and<br><blockquote type="cite">Matrix : Set -> Nat -> Nat -> Set<br></blockquote><blockquote type="cite">Matrix A n m = Vec (Vec A n m)<br></blockquote>The first are called deconstructors (or?) </div></blockquote><div><br></div><div>what?</div><br><blockquote type="cite"><div>but what are the second<br>called and what are they typically used for? </div></blockquote><div><br></div><div>Why do you need special names for things?</div><br><blockquote type="cite"><div>Functions beginning with<br>"Set" seems to only accept 1 pattern/1 value for Set. Is it so?<br></div></blockquote><div><br></div><div>You can't match on Set.</div><br><blockquote type="cite"><div><br>23. Am I correct in assuming that mixfix syntax demands that I got at<br>least 1 symbol between each argument, i.e.<br><blockquote type="cite">data _ _][ : Bool -> Bool -> Set where<br></blockquote><blockquote type="cite"> testing : (x : Bool) -> (y : Bool) -> x y ][<br></blockquote>isn't permitted (I know the above isn't permitted, I'm just wondering<br>if I can somehow do something about my syntax to make something<br>similar)?<br></div></blockquote><div><br></div><div>Yes.</div><div><br></div><br><blockquote type="cite"><div><br>24. What are the scoping rules in Agda? Using functions, data types<br>and postulated values before they are defined doesn't seem to be OK.<br>Is it always top-down or can I somehow make functions be aware of<br>functions declared further down?<br></div></blockquote><div><br></div><div>Yes, use mutual then indent. All the definitions then can be mutual recursive.</div><div><br></div><div>Actually it is a bit more subtle...</div><br><blockquote type="cite"><div><br>OK. It turned out to be more questions than I initially thought. Some<br>structured, some not so structured. I'll continue to tinker with Agda<br>but any guidance would be much appreciated.<br></div></blockquote><div><br></div><div>Tinkering is good. Have fun.</div><div><br></div><div>Thorsten</div><br><blockquote type="cite"><div><br>-- Oscar<br>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br></div></blockquote></div><br></body></html>