/home/laney/.irssi/irclogs/Freenode/#agda.log-20170804

--- Day changed Thu Aug 03 2017
rntzhm. there are release notes for agda version 2.5.303/08 14:21
rntzbut the git repo doesn't have a tag v2.5.303/08 14:22
rntzwut?03/08 14:22
rntzhow do I get agda 2.5.3? I was planning on using stack to build it from the git repo. I guess I could just try building HEAD...03/08 14:22
apostolisIt is not released yet.03/08 14:22
rntzah. the release notes are just a work in progress, then?03/08 14:23
rntzhttps://github.com/agda/agda/blob/master/CHANGELOG.md <- I mean these03/08 14:23
apostolisI guess.03/08 14:23
gallaisrntz: git checkout stable-2.503/08 14:24
gallais2.5.3 has not been released yet. It's the "stable" dev version03/08 14:24
gallais(as opposed to 2.6.0 in which you have wildly new features like support for cubicaltt)03/08 14:25
rntzI see, thanks.03/08 14:25
joel135I am reading an intro to agda.03/08 16:34
joel135Why "data Vec (A : Set) : Nat -> Set where" instead of "data Vec : (A : Set) -> Nat -> Set where"?03/08 16:35
joel135Will Vec have the latter type when the former construct is used?03/08 16:38
glguyjoel135: Type "parameters" go to the left of the : and type "indexes" go to the right03/08 16:38
glguyThe named parameters are in scope while defining the constructors while the named indexes are only in scope within the type03/08 16:39
joel135Ok thanks03/08 16:40
glguydata TwoA : (A1 : Set) → Set where two : (A2 : Set) → A → A → TwoA A03/08 16:42
glguydata TwoB (A : Set) : Set where two : A → A → TwoB A03/08 16:42
glguyOh, and I meant to rename the A's in TwoA to A@03/08 16:43
glguyA203/08 16:43
joel135Ok so if there is no interaction between different assignments to the same variable then it can be made into a parameter.03/08 16:47
joel135TwoA and TwoB are pretty much equivalent, right?03/08 16:50
glguyjoel135: Yeah, the parameters will be used uniformly by all of the constructors. It's only the indexes that allow flexibility03/08 16:50
glguyYeah, they're similar except that one has 3 fields and one has 203/08 16:51
joel135Yes03/08 16:52
gallaisglguy: TwoA cannot have the type it claims to have because the constructor "two" takes "A2" (a "Set") as an argument03/08 17:03
gallaisSo "TwoA" has to be larger than "Set" to avoid inconsistencies ("Set 1")03/08 17:03
gallaisWhereas when you are using a parameter, you don't have this issue03/08 17:04
glguygallais: I loaded it in Agda before I pasted it03/08 17:04
glguygallais: You're right about that in general, but Agda appears to be more clever now03/08 17:05
joel135It is possible to express that constructors are distinct? Or is that usually not needed?03/08 17:07
glguygallais: Now if we change the definition to: data TwoA : Set where twoA : (A2 : Set) → A2 → A2 → TwoA03/08 17:07
glguygallais: At this point we'll get the error about the sizes of Set and Set103/08 17:07
glguyjoel135: constructors are always distinct03/08 17:07
joel135Can it be expressed in the type system?03/08 17:08
glguyWhat?03/08 17:08
joel135I don't know. I guess it is unnecessary.03/08 17:08
glguydata Example : Bool → Set where example1 : Example true; example2 : Example false03/08 17:09
glguyMaybe that's what you mean?03/08 17:09
gallaisI guess Agda has detected it as a parameter then03/08 17:10
gallaisjoel135: if you have a proof of true = false, you can pattern match on it using the absurd pattern () and that'll prove anything03/08 17:11
gallaissame for any other "c1 (..) = c2 (..)"03/08 17:11
gallaiswhere c1 and c2 are two distinct constructors03/08 17:11
joel135Ok that's what I was after.03/08 17:12
gallaishttps://agda.readthedocs.io/en/latest/language/function-definitions.html?highlight=absurd#absurd-patterns03/08 17:13
joel135And my text apparently covers absurd patterns.03/08 17:13
dolioglguy, joel135: At this point, agda will figure out that the latter Vec is the same as the former if you write it correctly.03/08 17:22
dolioSo the only difference is some syntactic convenience, I think.03/08 17:22
joel135Does agda have cumulative universes?03/08 17:37
glguyjoel135: No03/08 17:57
joel135Are there terms with multiple types?03/08 18:05
joel135(Implicit arguments don't count.)03/08 18:06
mietekjoel135: 03/08 18:18
mietekabout your earlier question03/08 18:18
mietekdata FooBar : Set where foo bar : FooBar03/08 18:18
mietekfoo≢bar : foo ≢ bar03/08 18:18
mietekfoo≢bar = λ ()03/08 18:18
mietekit’s absurd to consider constructors could be not distinct03/08 18:19
joel135Right03/08 18:41
dolioWell, agda assumes it's absurd. :P03/08 19:27
joel135Yes :P03/08 19:28
dolioOnce you add higher inductive types, it suddenly becomes not absurd.03/08 19:28
joel135Doesn't coma have that?03/08 19:28
joel135(I don't know what it is.)03/08 19:29
dolioWhat's coma?03/08 19:29
joel135Oh, it's related to hott?03/08 19:30
joel135Oh sorry :p that's my language, i meant agda of course03/08 19:30
dolioOh, I don't know if you can flip a switch for agda to have them. I'd guess not yet.03/08 19:31
joel135Ok03/08 19:31
joel135About using dots in pattern matching: "What is important is that there is a03/08 19:34
joel135unique binding site for each variable in the pattern." Is this mainly to make recursions easier to check for the compiler? I have heard it is hard to check totality in greater and greater generality.03/08 19:34
joel135Or maybe it is has to do with the cost/possiblity of comparing arguments for equality?03/08 19:35
rntzi'm having a problem with projection overloading in agda; the following doesn't work: https://gist.github.com/rntz/10397d4b78f1b8d62bdb66a78c96001e03/08 20:19
rntzif I have record A with a field `obj`, and a record B "descending" from A, is there any way to have (obj x) where x : B also work?03/08 20:20
rntzthat is, I want "obj" to be overloaded, so it works for both arguments of type A and of type B03/08 20:20
rntzI could create a "typeclass" just for this, but that seems a little heavyweight03/08 20:24
rntz(and also won't let me use "obj" as a copattern for defining values of type A)03/08 20:24
mietekB.obj works03/08 21:31
mietekmaybe open an issue?03/08 21:32
mietekdolio: yes, that’s what I meant :P03/08 21:32

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!