/home/laney/.irssi/irclogs/Freenode/2011/#agda/February.log

--- Log opened Tue Feb 01 00:00:42 2011
--- Day changed Wed Feb 02 2011
* pigworker is thinking of nuking his MacBook and reinstalling everything.02/02 09:51
pigworkerJust checking: does Agda (as on hackage) work ok with ghc 7?02/02 09:53
* Saizan tries02/02 09:54
Saizanno, it seems02/02 09:54
pigworkerthanks02/02 09:56
pigworkerI probably ought to use the same Agda that my class are using.02/02 09:56
pigworkerI also hear rumours of an emacs less rubbish than Aquamacs.02/02 09:57
pigworkerAlthough, personally, I enjoy Aquamacs' recently acquired inability to display unicode.02/02 09:58
npouillardpigworker: you may want to try homebrew instead of macports if you reinstall everything02/02 09:58
pigworkernpouillard: that was my next question02/02 09:58
npouillardI no longer use MacOS, but I tried it and was positively impressed02/02 09:59
pigworkerI'm sick of macports leaving everything borked. I'm sick of ps2pdf not working, etc.02/02 09:59
pigworkerPerhaps, one day, if I'm very very good, eating my greens, saying my prayers etc, I'll be able to install gtk2hs.02/02 10:00
npouillardpersonally I was sick of non-binary,non-central packaging system on MacOS02/02 10:00
pigworkerNo, that's crazy talk, isn't it?02/02 10:00
pigworkernpouillard: I'm not sophisticated enough to identify those as the issues. It just makes me cry.02/02 10:03
pigworkerBy the way, I plot to steer my class in the direction of this channel...02/02 10:05
npouillardanyway, about homebrew its not much different than macport (since it is a source distribution), but the community seems much more active02/02 10:10
pigworkerI've heard positive things about homebrew, and so far no screaming. I'll try it.02/02 10:14
freiksenetIn Common Lisp type system allows adding arbitrary predicates to type definitions, but that doesn't work in type inference, that only adds runtime check (IIRC). Is it possible to use arbitrary predicates as type specifiers for type inference?02/02 14:00
freiksenetbasically is it possible to deduce type rule from a function a -> Bool02/02 14:00
freiksenetnot in agda, generally, is there any type theory supporting such stuff?02/02 14:01
dolioThere are type features called refinement types that allow you to carve out subsets of existing types.02/02 14:06
dolioAlthough, you can emulate them to a degree in Agda.02/02 14:06
dolioInstead of T -> Bool, use T -> Set, with the empty type instead of false, and the singleton type instead of true.02/02 14:07
freiksenethm, interesting02/02 14:07
dolioThen, if P : T -> Set, Sigma T P is the type of pairs of elements of T, and proofs that the first element satisfies P.02/02 14:07
dolioWhich is essentially the subset of T that satisfies P.02/02 14:08
dolioSome type theories have a special universe Prop that can only contain such empty-or-singleton types for this purpose.02/02 14:09
dolioAgda even used to, but it never worked quite right.02/02 14:09
freiksenetdoesn't Coq uses Props?02/02 14:09
dolioYes, that is one example.02/02 14:09
freiksenetuse*\02/02 14:09
dolioAlso, since you mentioned Common Lisp, you should look at Qi.02/02 14:10
dolioIt has an actual static type system, and it might have something like refinement types.02/02 14:10
freiksenetI did look at it a bit02/02 14:10
freiksenetdolio: refinment types look very interesting, thanks02/02 14:29
--- Day changed Thu Feb 03 2011
copumpkinglguy_: what do you think of extending bitvector to do floating point math? :P03/02 19:08
nightChello everybody03/02 19:47
Saizanhi03/02 19:48
--- Day changed Fri Feb 04 2011
glguyWhere did the Agda repository move to?04/02 17:09
glguyI'm seeing an empty directory in code.haskell.org04/02 17:09
djahandarieThat's because code.haskell.org got screwed04/02 17:09
freiksenetagain?04/02 17:09
glguyI know that, but where is the repo now?04/02 17:09
dantentry http://www.cse.chalmers.se/~nad/repos/Agda/04/02 17:11
djahandarieSeems to be the latest or a close enough version04/02 17:13
glguyThanks, danten.04/02 17:13
wiresI read that someone is working on a Java implementation of Agda; is there code somewhere?04/02 22:59
Saizana backend, you mean?04/02 23:00
copumpkin:O04/02 23:00
wiresBackend like MAlonzo? I don't think so04/02 23:00
wires"Norio Kato" Specification of Agda-A (Java Agda) http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXIUPDATES04/02 23:01
--- Day changed Sat Feb 05 2011
kyagrdIs there a configuration file for Agda where I can specify ghc path?05/02 00:42
--- Day changed Sun Feb 06 2011
starcloudedhello everybody06/02 00:21
Saizangi06/02 00:21
Saizan*hi :)06/02 00:21
starcloudedhow can I debug a module in agda from emacs?06/02 00:23
copumpkindebug?06/02 00:24
starcloudedI want to test if a function I created do what it suposu to do06/02 00:30
copumpkinC-c C-n lets you "evaluate" an expression06/02 00:30
copumpkinso you could type in 5 + 6 <enter>06/02 00:31
copumpkinand it'd spit out 1106/02 00:31
starcloudedthanks06/02 00:31
starcloudedany ideas?06/02 00:49
glguyYou haven't asked a new qustion06/02 00:51
copumpkinwell, that was interesting06/02 00:59
starcloudedfor example when I try to add 5 + 7 the following message shows up06/02 01:08
starcloudedwhen checking that the expression 5 has type Nat06/02 01:08
starcloudedNo binding for builtin thing NATURAL, use {-# BUILTIN NATURAL name06/02 01:08
starclouded#-} to bind it to 'name'06/02 01:08
starcloudedwhen checking that the expression 5 has type Nat06/02 01:08
copumpkinyou need open import Data.Nat in scope06/02 01:08
copumpkinbut you can still call your own functions06/02 01:08
starcloudeddo I have to import Data.Nat if my program has this structure data Nat : Set where zero : Nat suc : Nat -> Nat06/02 01:11
starclouded_+_ : Nat -> Nat -> Nat06/02 01:11
starcloudedzero + m = m06/02 01:11
starcloudedsuc m + n = suc (m + n)06/02 01:11
starcloudedany ideas?06/02 01:21
Saizanno06/02 01:25
Saizanbut you've to define what the builtin natural and each constructors are if you want to be able to use numeric literals for it06/02 01:25
Saizanwith {-# BUILTIN NATURAL Nat #-}06/02 01:26
Saizan{-# BUILTIN ZERO zero #-}06/02 01:27
Saizan{-# BUILTIN SUC suc #-}06/02 01:27
starcloudedthanks for the help06/02 02:10
starcloudedsee ya06/02 02:10
starclouded\quit06/02 02:10
lispy_glguy: I got disconnect from minecraft.06/02 03:16
lispy_glguy: did that happen to you as well?06/02 03:16
glguyno06/02 03:20
glguyI'm still in06/02 03:20
lispy_glguy: hmm...my client crashed and it won't let me connect to the login server06/02 03:21
kfrHow practical is Agda? Can I do web dev in it?06/02 13:44
kfrWill Agda make me quit programming even faster than Haskell?06/02 13:44
Saizanwill you stop being such a troll?06/02 13:44
kfrI'm serious, how practical is it?06/02 13:52
kfrMy primary interest is concurrent stuff with sockets06/02 13:52
Saizansomeone posted a web framework to the mailing list some time ago, but i haven't looked into it06/02 13:53
Saizanthe I/O layer was probably done by with Haskell FFI06/02 13:53
kfrI know very little about Agda but I was looking into coming up with semantics for a programming language which makes runtime errors caused by the programmer largely impossible so I started out with simple stuff like how to prevent stuff like someList !! i from accessing something out of range06/02 13:54
kfrSo #esoteric told me to check out dependent types for that06/02 13:54
kfrAnd apparently Agda is the most popular example of that?06/02 13:54
SaizanCoq might be more popular, though Agda has a syntax much closer to haskell06/02 13:56
kfrAh, I see06/02 13:56
kfrBut I didn't really consider Coq becauswe I thought it was for proofs only really06/02 13:56
kfrAlthough edwardk said somebody wrote a self hosting Coq compiler06/02 13:56
Saizanno, you can write programs in both06/02 13:56
freiksenetkfr: i think usually people convert coq/agda code to more mainstream language like OCaml or Haskell06/02 13:57
kfrOh, are there already compilers for that?06/02 13:57
kfrSomebody told me that dependent types can hardly be implemented in Haskell06/02 13:58
kfrHow does that work out then?06/02 13:58
freiksenetCoq definetely converts to both Haskell and OCaml, IIRC06/02 13:58
Saizankfr: lots of unsafeCoerce in the generated code06/02 13:58
Saizan(agda also has a compiler backend that doesn't go through haskell)06/02 13:59
freiksenetkfr: another way is to write program in one language and then prove it in agda or coq06/02 14:01
raichookfr: I'll bite… what's impractical about haskell?06/02 14:32
kfrI'm not sure I ever said that Haskell was impractical06/02 15:22
raichookfr: Maybe i inferred it ;) 14:44:28 <kfr> How practical is Agda? Can I do web dev in it?06/02 15:23
raichoo14:44:44 <kfr> Will Agda make me quit programming even faster than Haskell?06/02 15:23
kfrType inference?06/02 15:23
raichooSomehow :P06/02 15:23
raichooBut I admit that my typechecker is inferior to those that are state of the art ;)06/02 15:24
kfrBut I suppose many people who come from the top 10 programming languages are not used to expressing programs in terms of nested functions/value oriented programming and that a function which reads a file and returns its constants has a return type of IO String instead of String or ByteString, managing structures using types in combination with StateT and such06/02 15:26
kfrAll very problematic06/02 15:26
raichooI can see that, there is a lot of skepticism when it comes to FP. I do scala in my dayjob and a lot of people are totally confused when i comes to high order functions. And monads scare the s**t out of them.06/02 15:28
kfrWow, you do Scala professionally? That's a first for me06/02 15:29
raichooI introduced it at my dayjob. Actually it's a test-ballon. But my boss seems to receive it very well.06/02 15:29
kfrDoes Scala have monads, too?06/02 15:30
raichooEvery language has ;)06/02 15:30
raichooBut it's not as explicit about it as haskell06/02 15:30
raichooYou have however for-comprehensions that resemble haskell do-notation.06/02 15:31
kfrraichoo what is the primary langauge you use at work?06/02 15:32
kfrI mean usually?06/02 15:32
kfrJava?06/02 15:32
raichooC++.06/02 15:33
kfrClose enough06/02 15:33
raichooYes, both are utterly painful ^^06/02 15:33
kfrAt least C++ has typedef :p06/02 15:34
raichootrue, but it lacks proper garbage collection.06/02 15:34
kfrI miss a type statement whenever I deal with Java or C#06/02 15:34
kfrI'm not sure why it made never made it into those language06/02 15:35
kfrlanguages*06/02 15:35
kfr... *never made06/02 15:35
raichooI think C++0x will at least provide mechanisms to include GC. But honestly… i would not use C++ for another major project.06/02 15:36
kfrWhat would you need a GC in C++ for?06/02 15:36
kfrSo you don't delete manually anymore?06/02 15:36
kfrC++ is still my language of choice for low level stuff06/02 15:37
Saizanthis is not #c++ though06/02 15:38
kfrBut in general I'd prefer any language with static typing and sandboxed execution methods06/02 15:38
kfrBy that I meant no raw memory manipulation, pointers, etc06/02 15:39
kfrHaskell, Java are the only portable candidates really06/02 15:39
kfrIn C# you'd pretty much have to avoid anything .NET to achieve portability with mono06/02 15:40
raichooI've been a die hard C++ Coder since 98. Working with scala and haskell soured the experience for me. It's just painful. I'd rather use C for lowlevel stuff now. But anyway, this is offtopic.06/02 15:43
starcloudedhello everybody06/02 19:37
lispy_starclouded: hello06/02 19:38
starcloudedanyone could give a practical example of a term using the uit type?06/02 19:39
glguyunit?06/02 19:40
starcloudedups sorry yes unit type06/02 19:43
glguyisEven : ℕ → Set06/02 19:45
glguyisEven 0 = ⊤06/02 19:45
glguyisEven 1 = ⊥06/02 19:45
glguyisEven (suc (suc n)) = isEven n06/02 19:45
jsilvazuHi06/02 19:51
glguyHello06/02 19:52
starcloudedjsilvazu: hello06/02 19:52
starcloudedhello06/02 20:00
jsilvazuhello how can I use a builtin for example for using the operations between natural numbers06/02 20:11
Saizanare you referring to the BUILTIN pragma?06/02 20:13
jsilvazureally I dont know, my question is because I want to use the addition operator  and whe I execute "1 + 1" this message is shown "No binding for builin thing NATURAL...06/02 20:17
glguyYou are getting that message because you use the literal '1'06/02 20:17
Saizanyeah06/02 20:18
glguyand it doesn't know what your natural number type is06/02 20:18
glguyor what your zero or suc constructor are named06/02 20:18
Saizan{-# BUILTIN NATURAL Nat #-}{-# BUILTIN ZERO zero #-} {-# BUILTIN SUC suc #-} -- if you have data Nat where zero : Nat; suc : Nat -> Nat06/02 20:19
jsilvazuthe com´iler suggest me some builtin06/02 20:19
jsilvazuok thanks06/02 20:19
Saizanthen you'll be able to use numeric literals, and they will be desugared to those06/02 20:20
jsilvazuI write in the top of the file {-# BUILTIN ZERO zero #-} and I get this error message Parse error BUILTIN<ERROR> ZERO zero #-}06/02 20:25
Saizanmaybe you've to put them after the definition of Nat06/02 20:26
starcloudedMaybe if you import the Data.Nat I read something about it but I really dont know where it is06/02 20:28
Saizanor you could just write suc zero rather than 1 :)06/02 20:28
Saizanhttp://www.cse.chalmers.se/~nad/repos/lib/ <- here is the code for the standard library, btw06/02 20:30
Saizanthere you can find Data.Nat06/02 20:30
starcloudedcan anyone could define a term for a unit type?06/02 21:26
Saizanthe unit type should be inhabited by a single value06/02 21:27
Saizanin fact you can use _ and agda will fill in that single value for you06/02 21:28
glguydata Unit : Set where unit : Unit06/02 21:30
glguybut it is common to define it as an empty record06/02 21:30
starcloudedbut this definition is not for a datatype06/02 21:31
starcloudedcause I need to define a term for a unit type06/02 21:32
glguylike you have a homework assignment that states "define a term for a unit type"?06/02 21:32
starcloudedyes, but the thing I want to know if this assignment is well formulated?06/02 21:34
Saizanis that the exact phrasing?06/02 21:35
Saizanif so, maybe it's asking you to define a type with a single inhabitant without using data or record06/02 21:36
starcloudedthis is the assigment "define a term for *each* type shown in the file NonDependentTypes.agda. The shown types are ⊤, _×_, R, _+_, ..."06/02 21:36
Saizanok, then how is your ⊤ defined?06/02 21:37
starcloudedtop is defined as an unit type06/02 21:37
Saizani meant the agda code06/02 21:37
Saizan"record ⊤ : Set where" ?06/02 21:37
starcloudeddata ⊤ : Set where  -- to type ⊤ we type \top   tt : ⊤06/02 21:39
Saizanah, so just tt will work06/02 21:39
Saizane.g. "term-⊤ : ⊤; term-⊤ = tt"06/02 21:40
starcloudedSaizan: thanks so the assignment was well formulated?06/02 21:43
Saizanyep06/02 21:43
starcloudedSaizan: a term definition for "data _×_ (A B : Set) : Set where; _,_ : A → B → A × B" what it should be?06/02 21:56
freiksenetduh, I wish our school cirriculum included Agda courses06/02 21:58
Saizanstarclouded: and expression of type  ⊤ × ⊤ for example06/02 21:59
starcloudedbut how can define the type expression of my new term?06/02 22:02
Saizani don't understand your question06/02 22:02
starcloudedthe idea of this term definition is to give a map of the conduct of the values using types, no? what is the type of the parameters and what is the type of the output06/02 22:06
starclouded?06/02 22:06
Saizanthere are no parameters because these are not function types06/02 22:08
Saizanthe "output" has to mention _×_, so it should be something like ⊤ × ⊤ becuase _×_ itself is a parametrized type whihc takes two arguments06/02 22:10
starcloudedit should be something like this "term-× : ⊤ → ⊤ → ⊤ × ⊤"06/02 22:13
starcloudedSaizan: some help please?06/02 22:28
starcloudedit should be something like term-x : T x T; term-x = term-T , term-T ????06/02 22:35
Saizanyep, looks right06/02 22:38
starcloudedSaizan: thanks men06/02 22:47
starcloudedin the term definition in the record type is there a special for separating each element of the n-tuple?06/02 22:59
Saizan;06/02 23:00
starclouded; and then a space?06/02 23:01
copumpkinspaces everywhere06/02 23:02
copumpkinthe parser doesn't like compressed code06/02 23:03
copumpkin:P06/02 23:03
starcloudedyes I forget the spaces before }06/02 23:05
starcloudedthe code compile with this record type but message appears like a warning or something like "(A B C : Set) → Set !=< _4 of type Set₁ when checking that the expression R has type _4" ?06/02 23:07
starcloudedby the datatype is like this "record R (A B C : Set) : Set where; field;  f₁ : A;  f₂ : B;  f₃ : C"06/02 23:08
Saizanwhich code is giving that error?06/02 23:11
starcloudedterm-R : R term-R = record {   f₁ = term-⊤   ; f₂ = term-×   ; f₃ = ℕ   }06/02 23:12
Saizanyou've to apply R to three type arguments there06/02 23:12
Saizanalso, you can't use ℕ for f₃06/02 23:13
starcloudedok, but how can I apply R to the three type arguments?06/02 23:15
Saizane.g. term-R : R ⊤ (T x T) ⊤; ...06/02 23:17
starcloudedI don`t get it . .06/02 23:21
Saizanstarclouded: think of R as a function that takes 3 types as arguments and produces a type06/02 23:23
Saizanit's really the same as _x_, except that it takes 3 arguments instead of 206/02 23:24
glguyIs the source file to the homework assignment online somewhere?06/02 23:24
starcloudednop06/02 23:25
copumpkinagda, as homework??06/02 23:25
copumpkinwhere?06/02 23:25
starcloudedI could send you if want06/02 23:26
glguyYeah, I'm curious06/02 23:30
starcloudedtell where I could send06/02 23:32
starcloudedSaizan: but when I put term-R = record { ... is not enough?06/02 23:37
--- Day changed Mon Feb 07 2011
starcloudedgood bye every body07/02 00:07
starcloudedhello everybody07/02 02:47
starcloudedanyone could give an example of a term definition for a function datatype?07/02 03:07
glguyYou have weird homework07/02 03:08
codolioIt sounds like good homework.07/02 03:09
codolioExcept, i don't know what that means.07/02 03:10
glguymaybe it just means "define a value whose type is a function"?07/02 03:13
glguyand you just have to define any function07/02 03:13
djahandarieAsking about Agda homework in #agda is dangerous07/02 03:15
djahandarieBecause it is fairly probable that whomever assigned it is also in the channel07/02 03:15
glguyIf dolio doesn't understand the question the homework is asking, it's likely that the question is wrong and worth asking about on #agda :)07/02 03:20
dolio:)07/02 03:20
starcloudeda term of a list could be the head of the list?07/02 03:56
copumpkin?07/02 04:14
copumpkinstarclouded: where are you that teaches agda, by the way?07/02 04:14
starcloudedColombia07/02 04:15
djahandarieRepublic of Colombia? O.o07/02 04:30
starcloudedyes07/02 04:31
starcloudedgood night to all07/02 05:14
--- Log opened Mon Feb 07 13:57:43 2011
-!- Irssi: #agda: Total of 31 nicks [0 ops, 0 halfops, 0 voices, 31 normal]07/02 13:57
-!- Irssi: Join to #agda was synced in 68 secs07/02 13:58
--- Log closed Mon Feb 07 13:59:43 2011
--- Log opened Mon Feb 07 14:12:07 2011
-!- Irssi: #agda: Total of 30 nicks [0 ops, 0 halfops, 0 voices, 30 normal]07/02 14:12
-!- Irssi: Join to #agda was synced in 71 secs07/02 14:13
freiksenethow exactly do implicit arguments work? Do they just become "explicit" after the type checking stage (so agda puts as function arguments) or is there some other mechanism on how they are applied?07/02 14:26
Saizanthey get filled in during type checking, but it seems the internal representation still knows what's implicit and what's not all the way down, though i've never looked at the code07/02 14:28
freiksenetI wonder why would it need to do that07/02 14:30
freiksenethm, I guess more sensible error messages?07/02 14:30
freiksenetSaizan: thanks07/02 14:30
Saizani think so, or for when it produces some code to insert into your file, like with C-c C-c and C-r07/02 14:31
npouillardwho goes to AIM-XIII ?07/02 14:36
starcloudedhello everybody07/02 14:58
starcloudedis there a special location inside a file _.agda to put an open import command?07/02 15:00
Saizanyou can put it anywhere you can put another declaration07/02 15:05
starcloudedthanks07/02 15:08
starcloudedhello everybody07/02 20:20
raichoohi starclouded07/02 21:33
starcloudedhi07/02 21:34
starcloudedgood bye everybody07/02 21:37
--- Day changed Tue Feb 08 2011
npouillardhttp://paste.pocoo.org/show/334209/ <= I would expect this to type-check, what do you think08/02 08:57
Saizannot sure, e.g. in haskell you've to say "import M hiding (T(..))" if you want to hide the constructors too08/02 09:02
npouillardSaizan: the point was to exploit the fact that one can reuse the same name for the constructors in agda08/02 09:04
Saizannpouillard: ah, right, with data G : Set where C : G it resolves the overloading just fine08/02 09:06
Saizanso it looks like a bug to me too08/02 09:07
npouillardok, thanks, I report it then08/02 09:08
npouillardhttp://code.google.com/p/agda/issues/detail?id=279 <= oh, looks like the same thing08/02 09:16
npouillardSaizan: what version do you have?08/02 09:16
glguy_  foo C = M.C08/02 09:21
glguy_type checks, fwiw08/02 09:21
npouillardglguy: thanks its the less ugly workaround08/02 09:28
npouillardglguy,Saizan: do you think adding my example would help #279, the status seems non-clear to me08/02 09:28
Saizanlooks like the first fix wasn't complete, so it's still open08/02 09:41
Saizani'm using the darcs version btw, not sure how recent since c.h.o is still not working properly08/02 09:42
npouillard<troll?> should we propose to switch to git? </troll?>08/02 10:03
Saizani'm in the "git tends to get in my way" camp08/02 10:17
SaizanMon Jan  3 12:00:01 CET 2011  Nils Anders Danielsson <nils.anders.danielsson@gmail.com> * Extended the Epic installation instructions.08/02 10:17
Saizanlast patch i have08/02 10:17
npouillardSaizan: Was in that camp, one year ago, and now git seems much lighter for branching/merging08/02 12:51
npouillardThe Yi project got there repo on c.h.o restored, they explicitely asked I think08/02 12:52
starcloudedhello everybody08/02 15:51
Saizanhi08/02 15:53
starcloudedin functional programming one could work with deductive databases like one can do logic programming?08/02 16:00
stevanhi, does this make sense: http://hpaste.org/43788/s , if so why?08/02 19:41
stevanannotated the type error also08/02 19:42
Saizanit makes sense only implementation-wise, each (λ ()) gets transformed into a distinct named definition, and then those get compared by "name"08/02 19:45
copumpkinwhy is that? it's bitten me before08/02 19:46
copumpkinit's sort of like where declarations08/02 19:46
stevanah, so a more fair comparison would be elim as it is and then elim2 : Fin 0 -> A and then try to prove elim == elim2?08/02 19:48
Saizani guess the main complication is that in general the given type might reference local variables08/02 19:48
Saizanstevan: right08/02 19:48
Saizanwhich you can't do, without extensionality08/02 19:49
stevanbut is there any problem having \() always be equal to any other \() ?08/02 19:49
Saizani don't know08/02 19:49
stevanhmm08/02 19:51
copumpkinmaybe post to mailing list about that and wheres?08/02 19:52
stevanwhat about wheres?08/02 19:53
Saizanwhere are simply annoying because you can't reference the function defined there when you try to prove things about the toplevel one08/02 19:54
copumpkinbut you also can't reproduce it08/02 19:55
copumpkinas far as I remember08/02 19:55
copumpkineven if it normalizes to the exact same code08/02 19:55
Saizanah, yeah, so it's the same problem that names matter08/02 19:56
stevani think i know what you mean, but can't come up with an example. got one?08/02 19:59
Saizanit comes up often with functions defined with well founded induction, e.g. the half examples in Induction.Nat in the standard library08/02 20:03
Saizan(though those would probably be a mess to prove things about anyway)08/02 20:04
stevan:-p08/02 20:05
Saizanone improvement would be to compare pattern matching definitions by the structure of their patterns and bodies, i think, with an hash that shouldn't be too expensive i hope08/02 20:08
stevani think i found the colombian couse using agda: http://www1.eafit.edu.co/asicard/teaching/dtfl-CB0683/  :-)08/02 23:17
--- Day changed Wed Feb 09 2011
dolioBoy, building agda with profiling is heinous.09/02 03:57
djahandarieYeah, yeah it is.09/02 03:58
copumpkinI tried that09/02 04:01
copumpkinbut it won't even build with my current GHC :(09/02 04:01
dolioI'm on file 173.09/02 04:02
dolioI wonder if there's a way to tell cabal to disable profiling specifically for agda.09/02 04:02
dolioSince I'm never going to debug it.09/02 04:02
dolioAnd I never remember --disable-library-profiling.09/02 04:03
kfish--disable-library-profiling-for-agda-plzthx09/02 04:04
dolioNo, making a different flag that I have to remember isn't going to help. :)09/02 04:05
djahandarieCould always turn off the profiling library building. :P09/02 04:09
djahandarie(Entirely)09/02 04:09
dolioI have no idea how to prove some of this univalent stuff...09/02 07:25
freiksenetI've asked in haskell, but they are busy with "pratical" stuff it seems :D is there any way to do HM style unification on "or" constraints, so that among "normal" constraints there are also ones from which only one has to be valid in order for type checking to succeed?09/02 11:01
freiksenetalternatively, maybe unification of intersection types can be done through normal constraints, but i can't figure how09/02 11:02
starcloudedhello everybody09/02 14:30
ccasinhi!09/02 14:31
q957hello09/02 15:22
q957i'm looking for a proof assistant09/02 15:23
q957i don't know if agda is good for what i have in mind09/02 15:23
djahandarieWell it is a proof assistant. :P09/02 15:23
q957i'd like to write down basic set theory proofs09/02 15:23
q957such as why there is just one empty set etc.09/02 15:23
q957is it possible with agda?09/02 15:24
q957i would start from zermelo fraenkel set theory09/02 15:25
Saizani think it's possible09/02 15:26
q957but aside from being possible, is agda the right tool? or is there some other proof assistant better suited?09/02 15:27
q957my needs are very simple. i just need first order logic09/02 15:27
ccasincoq is probably better suited09/02 15:27
Saizanif you're interested in how the proof look agda might be better than coq?09/02 15:28
ccasinboth systems are constructive, so you'll have to assume LEM (or some other classical axiom) in addition to ZF09/02 15:28
Saizan*proofs09/02 15:28
q957ccasin, what do you mean by LEM?09/02 15:28
ccasinlaw of the excluded middle09/02 15:28
q957of course. i'd like to use classic first order logic and natural deduction.09/02 15:29
djahandarieDoesn't assuming LEM in Agda make it inconsistent or something like that?09/02 15:29
Saizanno09/02 15:29
ccasindjahandarie: not any more09/02 15:29
ccasinas least, as far as we know09/02 15:29
ccasin*at least09/02 15:29
Saizanit ought not to :)09/02 15:30
ccasinIt will if you turn on --injective-type-constructors :)09/02 15:30
ccasinq957: I think either system will work fine09/02 15:31
ccasinAs Saizan suggests, agda might be better if you are interested in the computational structure of the proofs09/02 15:31
djahandarieI really wish these online mailing list viewer things would wrap the damn text09/02 15:31
ccasinwhereas coq might be better if you want to work quickly using more familiar reasoning techniques (though, for the same reason, it has a higher learning curve)09/02 15:32
ccasinthere has also already been some work done on set theory in coq, but I don't know of developments in agda09/02 15:32
q957but how does a basic proof in agda look like? for example, proving that the empty set is unique from the fact that two sets are the same if and only if they contain the same elements?09/02 15:33
ccasinthis depends on how you choose to formalize your axioms09/02 15:34
ccasinone option is just to add a type for sets and then the axioms as postulates09/02 15:35
q957in latex: \forall x\forall y ( x = y \leftrightarrow \forall z ( z \in x \leftrightarrow z \in y ) )09/02 15:35
ccasinfor example,09/02 15:35
ccasinpostulate zfset : Set09/02 15:35
ccasinpostulate in : zfset -> zfset -> Set09/02 15:36
ccasinsorry,  one second09/02 15:37
ccasinthen, for example, you could assume extensionality as09/02 15:42
ccasinpostulate extensionality : (a b : zfset) → ((a = b) ⇔ ((z : zfset) → (in z a ⇔ in z b)))09/02 15:42
ccasinand go from there09/02 15:42
ccasinthere are lots of other ways to do it too09/02 15:42
ccasinIn either system, you are going to have to do some work to get acquainted with the logic and figure out how you want to formalize set theory09/02 15:43
ccasinso it's probably best to start with a tutorial09/02 15:43
q957so proofs are encoded using unicode?09/02 15:47
ccasinagda has the advantage that it works nicely with unicode identifiers, and there are many standard definitions using them09/02 15:47
copumpkinor disadvantage, if you dislike unicode :P09/02 15:48
ccasinthere is an emacs mode that allows you to type (roughly) latex and have it automatically translated to unicode09/02 15:48
Saizan⇔ is something that you can define within the language, btw09/02 15:48
* djahandarie 's terminal is not rendering these too nicely09/02 15:48
ccasinYes, it's just a pair of the individual implications - I think that one is in the stdlib, but I could be wrong09/02 15:49
Saizanproofs look like functional programs, if you want to use a theorem you name the function which represent its proof and pass the needed premises as arguments09/02 15:50
djahandarieI don't understand how product types correspond to forall and sum types correspond to exists. All this page says is "Using the curry-howard isomoprhism..." as an explanation09/02 15:51
djahandarieErr, dependent product and dependent sum I mean09/02 15:51
copumpkindjahandarie: well, take exists first09/02 15:52
Saizandependent product is a bit overloaded/confusing term09/02 15:52
copumpkinexists says that the type of snd depends on value of fst, right?09/02 15:52
copumpkinI mean dependent pair09/02 15:52
copumpkindjahandarie: if you look at that type through C-H lens, it means that the logical statement in snd is saying something about the value in fst09/02 15:53
copumpkinand that the value of snd is a proof of that logical statement09/02 15:53
Saizandata Sigma (A : Set) (B : A -> Set) : Set where _,_ : (x : A) -> B x -> Sigma A B -- dependent sum09/02 15:53
copumpkinso exists x. P(x) is simply a pair of some value that satisfies P, and a proof that it does09/02 15:53
djahandarieAh, got it09/02 15:54
copumpkinthe dependent function is the same reasoning09/02 15:54
copumpkinit's a function that takes any input value, and returns a proof about that input (i.e., a value whose type depends on the input)09/02 15:55
copumpkinforall x. P(x) means that for any input value x, I can provide a proof that x satisfies P09/02 15:55
sullyTo quote the paper "All my friends' researchees are cooler than mine" on dependent types: "They are so powerful they can do ANYTHING."09/02 16:00
copumpkinoh it's a pigworker09/02 16:00
pigworkerI've got a tiny window of wifi on this train.09/02 16:01
djahandarieHmmm, I get it now09/02 16:03
copumpkinpigworker: any idea when and how long you'll be in the new cambridge, and whether you'd feel like meeting up with local haskellers? I'm sure we could get something arranged09/02 16:08
* djahandarie would attempt to go09/02 16:08
djahandarieBut I'm not very interesting. :P09/02 16:09
copumpkinshush :P09/02 16:09
copumpkinyou'd better start coming here09/02 16:09
djahandarieWell it's your fault you weren't there that time I did go!09/02 16:09
djahandarieLooks like that window wasn't very big.09/02 16:14
copumpkindjahandarie: having fun with agda?09/02 17:03
djahandarieNot yet :P09/02 17:03
djahandarieAlso I don't want to try compiling Agda on my laptop since it has overheating problems...09/02 17:04
copumpkinapart from their logical interpretations, dependent pairs and functions can be used to build other neat things09/02 17:04
copumpkinyou can build n-ary sums with dependent pairs09/02 17:04
copumpkinand n-ary (non-dependent) products with dependent functions09/02 17:04
djahandariedependent pair = Sigma,  dependent function = Pi ?09/02 17:05
copumpkinyeah09/02 17:05
copumpkinyou see how that would work?09/02 17:05
copumpkinin Haskell, Either a a ~ (Bool, a) ~ (AnyTwoElementType, a)09/02 17:07
djahandarieSigma n:N . (Fin n, a)? *shot in the dark*09/02 17:09
copumpkinnot quite09/02 17:09
copumpkinit doesn't have to be n-ary where n is a number09/02 17:10
copumpkindo you see the Either a a ~ (Bool, a) thing?09/02 17:10
djahandarieYes.09/02 17:10
copumpkinwhy is it a a? and not a b?09/02 17:10
djahandarieBecause the a is dependent on the Bool09/02 17:11
copumpkinyeah09/02 17:11
copumpkinso in agda, Either a b ~ Sigma Bool (\n -> if n then a else b)09/02 17:11
copumpkinbut there's nothing restricting you to just Bool09/02 17:11
djahandarieAh09/02 17:11
copumpkinyou can index it by anything you want, in any way you want09/02 17:12
copumpkinalong the same line of reasoning09/02 17:12
copumpkinin Haskell (a, a) ~ (Bool -> a)09/02 17:12
djahandarieHow would you work natural numbers into that (previous thing)?09/02 17:13
djahandarieWould you need to do something tricky because of the induction or whatever?09/02 17:14
copumpkinoh, not really09/02 17:14
copumpkinsay you want a sum indexed by a vector of types09/02 17:14
copumpkinwell, indexed by an index into a vector of types09/02 17:14
copumpkinfor true n-ary-ness09/02 17:15
copumpkinSum :: forall n. Vec n Set -> Set109/02 17:16
copumpkinSum {n} v = Sigma (Fin n) (\i -> lookup i v)09/02 17:16
copumpkin(using pseudo-haskell I guess)09/02 17:16
djahandarieAh, so you just use Vec so you don't need to deal with it09/02 17:17
copumpkinyeah, Vec can hold any universe level these days09/02 17:17
copumpkinso I can make a Vec of values, or a Vec of types, or a Vec of anything09/02 17:17
* djahandarie doesn't fully grasp what a universe is09/02 17:17
copumpkinit's like the kind/type distinction in haskell09/02 17:18
copumpkinexcept it keeps going09/02 17:18
copumpkinvalues have types09/02 17:18
copumpkintypes have kinds09/02 17:18
djahandarieLike System F?09/02 17:18
copumpkinkinds have ?09/02 17:18
copumpkinin Agda, you have value : SomeConcreteType09/02 17:18
copumpkinSomeConcreteType : Set09/02 17:18
copumpkinSet : Set109/02 17:18
copumpkinSet1 : Set209/02 17:18
copumpkinSet2 : Set309/02 17:18
copumpkinand it keeps going :P09/02 17:19
copumpkinbut to make things even nicer (in some ways)09/02 17:19
djahandarieHow do you define that?09/02 17:19
copumpkinthat number is actually (optionally) a parameter09/02 17:19
copumpkinso you can talk abstractly about any combination of universe levels09/02 17:19
copumpkindefine what?09/02 17:19
djahandarieSetX09/02 17:19
copumpkinjust the typing rules for it?09/02 17:20
djahandarieNo idea, it just seems too magical for me :P09/02 17:20
copumpkinit's no different from the type/kind boundary in haskell, except kinds in haskell are sort of neutered compared to types (ignoring the subtyping aspect of them)09/02 17:21
djahandarieIf byorgey's typekind thing happens, then will we have the same thing?09/02 17:21
copumpkinnot really09/02 17:21
copumpkinin agda, it's essential to have this for logical consistency09/02 17:22
djahandarieIn Haskell, no one cares about logical consistency!09/02 17:22
copumpkinif you have some "top" universe that is a member of itself09/02 17:22
copumpkinthen you get russell's paradox-like issues09/02 17:22
djahandarieWhat is (a, a) ~ to in Agda?09/02 17:26
copumpkinBool -> a09/02 17:26
copumpkinyou can write non-dependent functions just fine09/02 17:26
djahandarieErr, so (a,b) then :P09/02 17:26
djahandariePi Bool (\x -> if x then a else b)? :P09/02 17:27
copumpkin(x : Bool) -> if x then a else b09/02 17:27
djahandarieThat's nicer09/02 17:27
copumpkinPi gets special syntax in agda09/02 17:27
copumpkinespecially since it doesn't really have a type09/02 17:27
copumpkinor a type that can be described cleanly, anyway09/02 17:28
djahandarieCompared to Sigma, which does09/02 17:28
copumpkinyeah09/02 17:28
* djahandarie looks as the one written when this conversation started09/02 17:29
djahandarieWhy does it use Set? Isn't that limiting?09/02 17:29
copumpkinwhich one?09/02 17:29
djahandarie11:41 < Saizan> data Sigma (A : Set) (B : A -> Set) : Set where _,_ : (x : A) -> B x -> Sigma A B -- dependent sum09/02 17:29
copumpkinyeah, the one in the agda standard library is more flexible09/02 17:30
copumpkinworks at any universe level09/02 17:30
djahandarieAh, nice09/02 17:30
djahandarieI can't find it09/02 17:31
copumpkinData.Product in the standard library09/02 17:31
djahandarieAh nice, thanks09/02 17:31
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Product.html#21309/02 17:31
djahandarieAh, damn unicode09/02 17:31
copumpkinit's a record09/02 17:31
copumpkinmakes some things cleaner09/02 17:32
djahandarieSo a normal function type is like a less powerful Pi type?09/02 17:33
copumpkinyeah09/02 17:33
copumpkinit's a pi type that doesn't look at its input09/02 17:33
djahandarieRight09/02 17:33
copumpkinjust like a normal non-dependent pair is also a dependent pair that doesn't care about the first component09/02 17:34
djahandarieYeah09/02 17:34
copumpkin(a, b) ~ Sigma a (const b)09/02 17:34
djahandarieDependent types always start confusing me when I start thinking about runtime though09/02 17:34
copumpkinwell, the typechecker is (among other things) a huge partial evaluator of the language09/02 17:35
copumpkinso if I take our definition of Either from before09/02 17:35
copumpkinEither Int Bool ~ Sigma Bool (\n -> if n then Int else Bool)09/02 17:35
copumpkinso now if I write09/02 17:35
copumpkin? , ? in agda09/02 17:35
copumpkinthat is, a pair constructor with two holes09/02 17:36
copumpkinit'll actually make the holes into09/02 17:36
copumpkin{ }0 , { }109/02 17:36
copumpkinand if I ask the type of the first hole09/02 17:36
copumpkinit'll say it expects a Bool there09/02 17:36
copumpkinif I ask for the type of the second hole, it'll say it expects a type of if ?0 then Int else Bool09/02 17:36
copumpkinso now, I type true into { }009/02 17:36
copumpkinthen it's able to further evaluate the type of { }109/02 17:37
copumpkinand will resolve it to Int09/02 17:37
copumpkinso then I can safely write: true , 109/02 17:37
djahandarieSo if I don't have any of my values at compile time all the dependent type checking will need to move to runtime?09/02 17:37
copumpkinnope09/02 17:37
copumpkinthat's where the proofiness comes in09/02 17:37
copumpkinso basically, the only way you can construct one of these at runtime is by carrying a proof that your fst is a particular value09/02 17:38
copumpkinin practice, this case is trivial09/02 17:38
copumpkinyou can write left : A -> Either A B and put the constants into that09/02 17:39
copumpkinleft x = true , x09/02 17:39
copumpkinright : A -> Either A B09/02 17:39
copumpkinright x = false , x09/02 17:39
copumpkinthose bits typecheck and you can play with them as you please09/02 17:39
copumpkinhowever, in more sophisticated sigmas, you might need a more sophisticated proof that you have a particular fst and a snd that matches it09/02 17:39
djahandarieIsn't that just the same as providing the value at compile time?09/02 17:39
copumpkinyes, for that case09/02 17:40
copumpkinbut basically, the answer amounts to bringing "knowledge" of the fst of the pair into scope by pattern matching09/02 17:40
djahandarieSo like... "assume fst is this and work from there"?09/02 17:41
copumpkinyeah09/02 17:41
djahandarieThen every "path" is type checked so you know the whole program is valid09/02 17:41
copumpkinif you know which value you're going to provide, then you can give that knowledge to agda09/02 17:41
copumpkinif not, then you need to handle both cases09/02 17:41
copumpkinand then in each of those cases, agda acquired the knowledge of it being either09/02 17:42
copumpkinso yeah, as you say, every (possible) path is checked09/02 17:42
copumpkinsometimes it can get rather hairy09/02 17:42
djahandarieThis is pretty cool.09/02 17:44
copumpkinI love it, in case you hadn't noticed from my constant evangelizing in #haskell :P09/02 17:44
copumpkinwhat's even cooler is conor's recent tweet about letting these strong types guide your actual development09/02 17:45
copumpkinif you encode the invariants you care about in your datatypes, often the code will almost write itself09/02 17:45
copumpkinand will be pretty easy to prove things about, too09/02 17:45
copumpkinor easier, anyway :P09/02 17:45
djahandarieWhat do you mean by encode the invariants? I'm not sure I understand what invariant is here09/02 17:46
copumpkinanything at all, that you care about09/02 17:47
copumpkin:P09/02 17:47
djahandarieWhat if stuff I care about varies? :P09/02 17:48
copumpkinyou can let it vary :P09/02 17:48
* djahandarie questions the usage of the word invariant09/02 17:48
copumpkinthings like your red-black tree invariants, or the fact that in your language AST, all variables must exist in the context09/02 17:49
djahandarieHm, I kind of wish I saw your Agda intro copumpkin :P Considering that this is probably the most I learned about Agda and it was entirely painless, lol09/02 17:50
kosmikusthere's always surprisingly much that you don't want to vary :)09/02 17:50
copumpkindjahandarie: hah, it wasn't very good :P09/02 17:51
copumpkinI need to practice talking a lot more :)09/02 17:51
djahandarieMe too :(09/02 17:51
djahandarieAnyways, class now. o/09/02 17:51
copumpkinciao09/02 17:51
djahandarieThanks :)09/02 17:51
copumpkinnp :)09/02 17:51
kosmikuscopumpkin: you gave an Agda intro?09/02 18:21
copumpkinkosmikus: a bad one :)09/02 18:23
kosmikuswhere?09/02 18:30
copumpkinboston haskell meetup09/02 18:30
copumpkinquite a few haskellers in the area09/02 18:31
djahandarieI still need to remind edwardk to upload that video in a well-timed manner09/02 19:21
kosmikuscopumpkin: nice09/02 19:23
copumpkindjahandarie: not sure how good the video is, because he forgot his tripod and I think the camera spent most of the time on a table pointing in the wrong direction, but it may be better than nothing09/02 19:27
copumpkinmaybe double negative elimination applies09/02 19:27
copumpkina bad video of a bad talk makes for a good experience09/02 19:27
copumpkin:P09/02 19:27
djahandarielol09/02 19:28
kosmikus:)09/02 19:30
copumpkinI guess that isn't very constructive ;)09/02 19:56
djahandariecopumpkin, what is the use of postulates?09/02 21:57
copumpkinstuff you think is true but can't (be bothered to) prove09/02 21:57
copumpkinpostulate dne :: Not (Not e) -> e09/02 21:58
copumpkinhowever, it's not as useful as being able to prove it within the language, as obviously it has no computational behavior09/02 21:58
djahandarieWhat does it operationally do?09/02 21:58
copumpkinyou can postulate bottom :: a09/02 21:58
copumpkinit typechecks, and throws an error if you ever try evaluating it09/02 21:58
djahandarieAh. That feels somewhat useless.09/02 21:58
djahandarieOr, "bad to use" rather09/02 21:59
copumpkinpeople often postulate extensionality of function equality09/02 21:59
djahandarieIs it kind of like writing a type signature in Haskell and setting its value to undefined?09/02 22:00
copumpkinyeah, or error "you evaluated a postulate" as the value09/02 22:00
djahandarieI see09/02 22:01
djahandarieIt has to be done like this because Agda doesn't have bottom, right?09/02 22:01
copumpkinwell, you can write dne = dne09/02 22:01
copumpkinit'll turn pink09/02 22:02
copumpkinI dunno, I prefer parametrizing by what I postulate by09/02 22:02
copumpkinthan just postulating it09/02 22:02
copumpkinrather09/02 22:02
djahandarieDon't quite understand what that means09/02 22:02
copumpkininstead of postulating dne :: Not (Not e) -> e09/02 22:02
copumpkinpass (forall e. Not (Not e) -> e) as a parameter to anything that needs it09/02 22:02
copumpkinpossibly via a module parameter09/02 22:03
copumpkinit makes your requirements more explicit09/02 22:03
djahandarieAh. If you used a postulate you would instead just reference to the postulate inline with its name (dne)?09/02 22:04
copumpkinyeah, it's just a value09/02 22:04
copumpkinbut it doesn't normalize to anything09/02 22:04
copumpkinbut itself09/02 22:04
djahandarieOkay.09/02 22:04
copumpkinanyway, I have to run09/02 22:05
copumpkinbut I'll be back later09/02 22:05
djahandarieAlright, thanks09/02 22:05
pigworkercopumpkin: shortly after I was silently disconnected earlier, my irc client misled me into believing I had sent the following...09/02 22:10
pigworkerI'll be staying with Randy Pollack from the evening of Fri 11 Mar to sometime on Mon 14 Mar. Not sure what my hosts have planned for me, but would be happy to investigate possibilities.09/02 22:11
pigworkerre a Boston hookup09/02 22:11
starcloudedgood by everybody, today the chat was very illustrated09/02 23:02
--- Day changed Thu Feb 10 2011
copumpkinpigworker: great to hear that10/02 00:39
copumpkinpigworker: well, if you have free time and feel like hanging out, just ping me or say so on twitter and I'll see how many people I can pull together10/02 00:39
pigworkerI'm sure more of a plan will emerge nearer the time. It'd be cool to hook up.10/02 00:40
copumpkindjahandarie: how goes the agda-ing?10/02 00:50
djahandarieDormant.10/02 00:52
djahandarieI should work on getting an actual Agda compiler/environment working10/02 00:53
djahandarieWould probably be easier to learn if I had one...10/02 00:53
* djahandarie wonders why he hasn't done this earlier10/02 00:53
copumpkinjust grab an ice pack and stick it under your laptop if it overheats10/02 00:53
copumpkinI actually used to do that on my old laptop10/02 00:53
djahandarieHaha, I have a desktop right now so I should be able to get something working :)10/02 00:54
copumpkinI'd go with the darcs version10/02 00:54
copumpkinunfortunately it doesn't build against GHC head right now10/02 00:54
djahandarieWell dinner for now, I'll figure this out later :P10/02 00:57
revenantphxalright copumpkin, you've dragged me in10/02 02:45
djahandarieWelcome...10/02 02:45
djahandarieI'm just a noob in here too though :)10/02 02:46
copumpkin:)10/02 02:46
copumpkinso the imports and fixities should be pretty obvious, right?10/02 02:46
copumpkin(in agda you use _+_ instead of (+) to say it's infix)10/02 02:46
revenantphxokay10/02 02:46
djahandarieCan you do postfix?10/02 02:46
copumpkinmeaning you can write if_then_else_ and have it parse if p then x else y as if_then_else_ p x y10/02 02:47
revenantphx# is what?10/02 02:47
copumpkinyou can do any *fix you want10/02 02:47
djahandarieNeat.10/02 02:47
revenantphxuseful10/02 02:47
djahandarieSo I can define the syntax for [1,2,3,4]?10/02 02:47
copumpkin# is just syntax because I can't write numbers alone as identifiers10/02 02:47
copumpkin1# is an identifier, 1 is just a literal10/02 02:47
revenantphxoic10/02 02:47
revenantphxTapl's STLC defines t,v,T and gamma10/02 02:47
copumpkindjahandarie: in a roundabout way, by doing [_, _,_, and _], but that's ugly10/02 02:47
djahandarieHah10/02 02:48
copumpkindjahandarie: otherwise, no10/02 02:48
djahandarieNot exactly what I had in mind :P10/02 02:48
revenantphxterms, values, Types and contexts10/02 02:48
copumpkinrevenantphx: I haven't actually read tapl10/02 02:48
copumpkinanyway, the first real line of program10/02 02:48
copumpkindata Type : Set where10/02 02:48
copumpkinis just like a haskell GADT declaration, almost10/02 02:49
copumpkinSet is like haskell's * kind10/02 02:49
copumpkinit's the type of types10/02 02:49
copumpkinso I'm just creating a type called Type10/02 02:49
copumpkineach of the following 5 lines is making a constructor of that type10/02 02:49
revenantphxRemember when I was mentioning how I thought sets and types were similar >_>?10/02 02:50
revenantphxIs that relevant to agda's naming of * as Set?10/02 02:50
copumpkinyeah, types are definitely like sets10/02 02:50
revenantphx(also reminds me of ADA's definition of types actually)10/02 02:50
revenantphx(as ranges and suchs)10/02 02:50
revenantphxcarry on...10/02 02:50
copumpkinso 0# is a constructor, 1# is a constructor, and then the _+_ and _*_ and _=>_ are binary infix constructors10/02 02:51
copumpkinso I can write stuff like 1# + 1#10/02 02:51
copumpkin(note that I have no "interpretation" of the type yet)10/02 02:51
revenantphxwhich is equivalent to something like "succ"10/02 02:51
copumpkinit's not equivalent to anything really10/02 02:51
revenantphxA lot of examples I've seen implement 0, succ, prev for the number types.10/02 02:51
revenantphxcarry on >_>10/02 02:52
revenantphxsorry10/02 02:52
copumpkinin this case it's just an abstract representation of types10/02 02:52
revenantphx(ohey, zero, suc (derp))10/02 02:52
revenantphxRight.10/02 02:52
copumpkinI have 0#, the empty type, 1#, the unit type, and sums of types, products of types, and functions between types (also known as exponentials)10/02 02:52
revenantphxokay. :\10/02 02:52
copumpkinso 1# + 1# is a type with two values in it10/02 02:53
revenantphxah, okay10/02 02:53
copumpkin+ is like Either10/02 02:53
copumpkin* is like (,)10/02 02:53
copumpkinEither () () is roughly the same as Bool10/02 02:53
revenantphxand 1# x 1#?10/02 02:53
revenantphxoh, you meant tht by *10/02 02:53
copumpkinhow many interesting values of ((), ()) can you think of?10/02 02:53
copumpkinyeah, sorry10/02 02:53
revenantphx...not many10/02 02:53
copumpkinthere should be exactly one10/02 02:53
revenantphxactually, yeah10/02 02:54
copumpkin((0, ())10/02 02:54
copumpkin()10/02 02:54
copumpkinsorry10/02 02:54
copumpkin((), ())10/02 02:54
copumpkin(agda has no bottoms/undefineds)10/02 02:54
revenantphxso + is like either, x is a cartesian product of the types...10/02 02:54
copumpkinso => is an abstract representation of functions between these types10/02 02:54
revenantphxand i have no clue about =>10/02 02:54
copumpkinyeah, exactly10/02 02:54
revenantphx=> sounds like CT stuff.10/02 02:54
copumpkinnot at all10/02 02:54
copumpkinthis is basic arithmetic really10/02 02:55
copumpkinyou have 0, 1, plus, times, and => is "to the power of", backwards10/02 02:55
revenantphxoh, so you'd use => for type constructors?10/02 02:55
revenantphxOr am I just mixing stuff up more now.10/02 02:55
revenantphxI'm not getting the "to the power of" really.10/02 02:55
copumpkinwell, going back to haskell a moment10/02 02:55
copumpkinhow many functions () -> () can you think of?10/02 02:55
revenantphxer, they wouldn't be very useful.10/02 02:56
copumpkindoesn't matter10/02 02:56
copumpkinwhich ones could you write?10/02 02:56
revenantphxyou could write one that's just10/02 02:56
Philonous210/02 02:56
revenantphxblah () = ()10/02 02:56
copumpkinPhilonous: shush :P10/02 02:56
PhilonousSorry :>10/02 02:56
revenantphxcan't really think of anything else.10/02 02:56
revenantphxSince () can only really be one thing.10/02 02:56
copumpkinrevenantphx: and that's the only real one you can write, yeah10/02 02:56
copumpkinso () is almost equivalent to 1# in my code10/02 02:57
copumpkinthe type ()10/02 02:57
revenantphxunit type, gotcha.10/02 02:57
copumpkinhow about Bool -> ()?10/02 02:57
revenantphxTwo?10/02 02:57
copumpkinreally?10/02 02:57
revenantphxerm...10/02 02:57
revenantphxwell, only one really10/02 02:57
copumpkinyeah10/02 02:57
copumpkinjust think of what you can return10/02 02:57
revenantphxyou could write two I guess, but it doesn't matter where its true or false10/02 02:57
revenantphxk10/02 02:58
copumpkinit basically is forced to return ()10/02 02:58
copumpkinsince () has no other values in it10/02 02:58
revenantphxmmk10/02 02:58
copumpkinso if we're counting functions Bool -> (), we still only have one of them10/02 02:58
copumpkinin fact, for any type x, we can only write one x -> () function10/02 02:58
sullyone total function10/02 02:58
revenantphxI'm vaguely thinking of x^0 right now.10/02 02:58
copumpkinrevenantphx: it's actually 1^x10/02 02:58
revenantphxah okay10/02 02:58
revenantphxSo then for a bool to bool it should theoretically be 4?10/02 02:59
copumpkinbecause no matter what the input, you always have to return ()10/02 02:59
copumpkinexactly10/02 02:59
copumpkinand () -> Bool would be 210/02 02:59
copumpkinsully: yeah, I'm plugging my ears about bottoms and pretending they don't exist10/02 02:59
* copumpkin goes lalaalala10/02 02:59
sullythere are actually at least two "reasonable" haskell functions of type () -> ()10/02 02:59
revenantphxunsafeDoNothing?10/02 02:59
revenantphx>_>10/02 02:59
copumpkinsully: I'm just using haskell as an example to illustrate the STLC code :P10/02 02:59
djahandariesully, disregarding bottom?10/02 02:59
copumpkinsully: so bottoms really aren't relevant :P10/02 03:00
sullydjahandarie: no10/02 03:00
sullywhich STLC code?10/02 03:00
revenantphxI don't even know what a bottom is TT_TT10/02 03:00
djahandarieundefined10/02 03:00
copumpkinsully: this ugly code I threw together: http://pumpkinpat.ch/moo.html10/02 03:00
copumpkinrevenantphx: anything undefined or non-terminating or error-throwing10/02 03:00
copumpkinrevenantphx: but anyway, that isn't important here10/02 03:00
revenantphxok10/02 03:00
copumpkinso the basic point is that if I have (1# + 1# + 1#) => (1# + 1#)10/02 03:00
revenantphxso a => b , where a and b are types, will produce a^b possible (function) types?10/02 03:01
copumpkinb^a10/02 03:01
copumpkinnot function types, but function values10/02 03:01
revenantphxb^a >_<10/02 03:01
copumpkinso just back to sets10/02 03:01
revenantphxalright.10/02 03:01
copumpkinyou have A and B, and functions A -> B10/02 03:01
copumpkin| | is size of the set10/02 03:01
copumpkin|A -> B| = |B|^|A|10/02 03:02
copumpkin|A + B| = |A| + |B|10/02 03:02
copumpkin|A * B| = |A| * |B|10/02 03:02
revenantphxmmk10/02 03:03
copumpkinanyway, the size of the types isn't really too important here, but I just wanted to justify the naming a bit10/02 03:03
revenantphxWell I've learned something, so it's all good.10/02 03:03
revenantphxCarry on then ^_^10/02 03:03
copumpkinso basically, a lambda calculus is something that looks something like haskell :P to simplify things, we have lambdas but only allow one parameter at a time10/02 03:04
copumpkinand you can apply things, and that's about it10/02 03:04
copumpkinso (\x -> x) y is an expression in a lambda calculus10/02 03:04
copumpkinand simplifies to just y10/02 03:04
revenantphxright, this I've seen somewhat.10/02 03:04
copumpkinalright10/02 03:04
copumpkinyou can do all sorts of funky stuff like (\x -> x x) (\x -> x x)10/02 03:04
copumpkinwhich is a self-replicating expression10/02 03:05
revenantphxyeah, I was about say...10/02 03:05
revenantphxthat seems a bit...10/02 03:05
copumpkinhowever, types prevent most things like that :)10/02 03:05
revenantphxhurray for types.10/02 03:05
copumpkinanyway, one pretty common way to represent lambdas10/02 03:05
copumpkinor more specifically, lambda-bound variables (like the x above)10/02 03:05
copumpkinis by something called a de bruijn index10/02 03:05
copumpkinwhich basically counts how many lambdas away the variable was defined10/02 03:06
copumpkin(often starting from zero)10/02 03:06
revenantphxmmk...10/02 03:06
copumpkinso instead of writing (\x -> x) y, I could write (lambda. 0) y, because that x was only defined 0 lambdas away10/02 03:06
copumpkinif I had (\x -> (\z -> x z))10/02 03:07
copumpkinthat would be (lambda. (lambda. 1 0))10/02 03:07
copumpkinbecause in the inner scope, the x was defined one lambda away, and the z was defined 0 lambdas away10/02 03:07
copumpkinnot sure if this is making much sense10/02 03:08
revenantphxone moment10/02 03:08
sullycopumpkin: I have a t-shirt that reads "For a good time, call (\x.xx)(\x.xx)."10/02 03:08
copumpkinlol10/02 03:08
copumpkinrevenantphx10/02 03:09
revenantphxyeah sorry back10/02 03:09
copumpkinI can give more examples to help you see a pattern if you want10/02 03:09
revenantphxsure10/02 03:09
revenantphxi'm kind of just staring at it right now.10/02 03:09
revenantphxI'm not sure why it's useful I guess.10/02 03:09
copumpkin(\x -> (\z -> x z) (\y -> y x) x)10/02 03:09
copumpkinit's to avoid dealing with variable names in code that processes this10/02 03:10
copumpkinnames are ugly, and you don't want to have to deal with shadowing of names and such10/02 03:10
revenantphxmmk10/02 03:10
copumpkinthis is nice and unambiguous10/02 03:10
copumpkinso the one I just wrote is10/02 03:10
copumpkin(lambda. (lambda. 1 0) (lambda. 0 1) 0)10/02 03:10
copumpkinthe more nested lambdas you get, the higher those numbers go10/02 03:11
revenantphxoooh, since you can only have one input per lambda10/02 03:11
revenantphx>_< derp10/02 03:11
revenantphxYeah I tsee now.10/02 03:11
copumpkinokay10/02 03:11
copumpkinso now you get de bruijn variables10/02 03:11
copumpkinor indices10/02 03:11
revenantphxhow is bruijn pronounced btw?10/02 03:12
revenantphxsounds dutch.10/02 03:12
copumpkinit is10/02 03:12
copumpkinI've heard it said as de broin10/02 03:12
copumpkinlike groin10/02 03:12
copumpkinor de brine10/02 03:12
copumpkinor somewhere in between :P10/02 03:12
* copumpkin isn't dutch so doesn't really know10/02 03:12
revenantphxlike "brow-eh-n" with a lisp >_>10/02 03:13
revenantphxIf you combined them.10/02 03:13
kulakowskipeople will know what you mean10/02 03:13
revenantphxThat sounds weird though.10/02 03:13
copumpkin:)10/02 03:13
revenantphxAnyways, carry on, it's not important.10/02 03:13
djahandariekulakowski, not, I'm sure it'll be too ambiguous with the other name that sounds exactly like it since it's fairly common sounding. :P10/02 03:13
copumpkinrevenantphx: anyway, I'll start by saying that the Var type I define up there is roughly the de bruijn indices I just talked about, except a little fancier to be more typesafe10/02 03:13
copumpkinrevenantphx: I'll go more into detail in a bit, but I want to get to Expr first10/02 03:13
revenantphxok10/02 03:13
copumpkinyou'll notice that it looks like a natural number, as you might expect. It has two constructors, one for zero, and the other for successors10/02 03:14
copumpkinits type is just way fancier10/02 03:14
revenantphxwait, there's no Expr on that10/02 03:14
copumpkinoh sorry10/02 03:14
copumpkinI called it Term in there10/02 03:14
revenantphxk10/02 03:14
copumpkinso Term is a type with two parameters10/02 03:14
PhilonousMay I recommend Hindley, Seldin "Introduction to Combinators and Lambda calculus", it's a great book on the topic10/02 03:14
revenantphxalso whaty you just described sounds like Var10/02 03:14
revenantphxit has zero and suc :P10/02 03:14
copumpkinyeah, that's what I was describing10/02 03:14
copumpkinI just wanted to give you a basic intuition for what it was before moving on10/02 03:15
copumpkinI'll get back to it in a bit10/02 03:15
revenantphxyeah yeah sorry10/02 03:15
copumpkinno problem :P10/02 03:15
revenantphxI think IRC transposed messages.10/02 03:15
revenantphxso Term then.10/02 03:15
copumpkinso Term has a constructor var that embeds that other Var type I mentioned. I'll skip that too for now10/02 03:15
revenantphxim not clear on the sigma10/02 03:16
revenantphx(or the t and gamma, but I recall "type" and "context")10/02 03:16
copumpkinyeah, so first things first actually10/02 03:16
copumpkindata Term : Context → Type → Set where10/02 03:16
copumpkinthat means that Term is a type constructor10/02 03:16
copumpkinand it has "parameters" a context, and a type10/02 03:17
copumpkinwe say that it's "indexed" by them10/02 03:17
copumpkinmeaning that individual constructors get more say in what those parameters are10/02 03:17
revenantphxHate to say it, but you lost me.10/02 03:17
revenantphxI think it's the syntax10/02 03:17
copumpkinso in haskell10/02 03:18
revenantphxwhat is A { ... } representing?10/02 03:18
copumpkinthat would be10/02 03:18
copumpkindata Term :: * -> * -> * where10/02 03:18
copumpkinor data Term a b where10/02 03:18
djahandarierevenantphx, he hasn't gotten there yet.10/02 03:18
revenantphxOh, right10/02 03:18
revenantphxthat I got.10/02 03:18
copumpkinokay10/02 03:18
copumpkin  unit : ∀ {Γ} → Term Γ 1#10/02 03:18
copumpkin{} means an implicit parameter10/02 03:18
copumpkinwhich corresponds pretty closely here to how haskell uses forall10/02 03:18
copumpkinin Haskell, that would probably be Unit :: forall g. Term g 1#10/02 03:19
revenantphxalright...10/02 03:19
copumpkinnote the 1# in the Term there, which goes back to what I said about the constructor having "a say" in the parameters to the type10/02 03:19
sullyre de bruijn pronunciation10/02 03:19
sullyTAPL says that it is closer to "de brown" than to "de broyn"10/02 03:20
copumpkinah, interesting10/02 03:20
revenantphxah okay10/02 03:20
sullyalthough I think I say de broyn more often10/02 03:20
sullyalthough I have been trying to catch myself10/02 03:20
sullyas I don't want to impart bad habits on the students in the class I am TAing...10/02 03:20
copumpkin:)10/02 03:21
copumpkinrevenantphx: so, what that unit constructor is saying is that there's a "value" (Term) of type 1#10/02 03:21
revenantphxWhat exactly is in gamma here?10/02 03:21
copumpkinmy Type type was describing a language of types10/02 03:21
revenantphxRight, I got that.10/02 03:21
copumpkinmy Term type is describing a language of terms and their relationship to the type language10/02 03:21
copumpkinthe gamma is the context, which I'll get to in a bit10/02 03:21
djahandarierevenantphx, it's a free variable, like  x10/02 03:21
copumpkinbut yeah, here it's just anything10/02 03:22
copumpkinthe unit constructor doesn't care10/02 03:22
djahandarieunit : forall {x} -> Term x 1#   -- getting rid of unicode10/02 03:22
revenantphxright okay then10/02 03:22
copumpkinit just passes it on unchanged, basically10/02 03:22
copumpkinokay, now for a slightly scarier type10/02 03:22
copumpkin  inj₁   : ∀ {σ τ Γ} → (x : Term Γ σ) → Term Γ (σ + τ)10/02 03:22
copumpkinlet me rewrite that in haskell10/02 03:23
revenantphxalright.10/02 03:23
copumpkinLeft :: forall a b g. Term g a -> Term g (Either a b)10/02 03:23
revenantphx...Left?10/02 03:23
copumpkindata Either a b = Left a | Right b10/02 03:24
copumpkinjust convention :)10/02 03:24
revenantphxWhat is inj supposed to stand for?10/02 03:24
revenantphxOut of curiosity?10/02 03:24
copumpkininjection10/02 03:24
revenantphxk...10/02 03:24
copumpkinstick one of a or b into Either a b10/02 03:24
copumpkinbasically forget (type-wise) which of the two it was10/02 03:24
revenantphxso sigma and tau are just random variable names here?10/02 03:25
copumpkininj2 is the Right10/02 03:25
copumpkinyeah, I just was showing off the unicode in the pretty printer10/02 03:25
revenantphxI kind of get it I guess.10/02 03:25
copumpkinthat's the only reason that page is up there10/02 03:25
copumpkinso inj1 and inj2 are giving us a way of constructing an Either type (called + in that code)10/02 03:25
copumpkinnow we need a way of taking it apart10/02 03:26
copumpkin:t either10/02 03:26
lambdabotforall a c b. (a -> c) -> (b -> c) -> Either a b -> c10/02 03:26
revenantphxOn a side note, I just set it up so I can alt-space to switch input sources10/02 03:26
revenantphxi10/02 03:26
revenantphxincluding a unicode one :)10/02 03:26
revenantphxshould be useful10/02 03:26
copumpkin:P yeah10/02 03:27
copumpkinin agda-mode you can type unicode pretty easily10/02 03:27
copumpkinanyway, the haskell either function above is a fairly standard way of taking apart the Either type10/02 03:27
revenantphxall it does is clear off all the alt-<x> shortcuts, and let you do alt - x y z w10/02 03:27
copumpkinthe either constructor in my Term is roughly the same idea10/02 03:27
revenantphxAlright.10/02 03:27
copumpkinbut how it does that might be a little scary10/02 03:27
copumpkinI suppose I should talk about that context now :P10/02 03:27
revenantphxmm...10/02 03:27
copumpkinContext = List Type10/02 03:28
copumpkinthat was up there10/02 03:28
copumpkinwhat it does is track what variables are in scope10/02 03:28
copumpkinor more precisely, their types10/02 03:28
revenantphxah ok10/02 03:28
copumpkinso every time I make a lambda10/02 03:29
copumpkinI'm putting another variable in context10/02 03:29
revenantphxso each "index" in the list is tied to the de bruijn index or w/e10/02 03:29
revenantphx?10/02 03:29
copumpkinyeah10/02 03:29
copumpkinzero would be the head of the list10/02 03:29
revenantphxso the type of w/e is 3 away is at index 3 of the context.10/02 03:29
copumpkinyeah10/02 03:29
revenantphx(or 2, w/e)10/02 03:29
copumpkinyeah, I'd count from 0 in both cases10/02 03:30
copumpkinbut yeah, you get the idea10/02 03:30
copumpkinso let's take a look at the simplest case of this10/02 03:30
copumpkin  lam : ∀ {σ τ Γ} → (q : Term (σ ∷ Γ) τ) → Term Γ (σ ⇒ τ)10/02 03:30
revenantphxwhats the (x : ... notation?10/02 03:30
copumpkinit's just a way for me to name things in agda. otherwise when I pattern match on it (or ask agda to do that automatically) it generates an ugly name10/02 03:31
revenantphxI... see?10/02 03:31
djahandarie: is "type of", everywhere in the code.10/02 03:31
djahandarieUh10/02 03:31
djahandarielol10/02 03:31
djahandarie"has type"*10/02 03:31
copumpkinrevenantphx: so I named the parameter to the lam constructor q10/02 03:31
copumpkina good name, I know10/02 03:32
revenantphxcopumpkin: sounds fine >:P10/02 03:32
revenantphx:P*10/02 03:32
copumpkin:P10/02 03:32
copumpkinanyway, that type is saying10/02 03:32
revenantphxalso, ∷?10/02 03:32
djahandarieCons10/02 03:32
copumpkinyeah, it's just cons on List10/02 03:32
revenantphxah, okay, makes sense.10/02 03:32
djahandarie:: and : are switched in Agda from what they are in Haskell10/02 03:32
revenantphxaaah, gotcha10/02 03:32
copumpkinlam is a constructor that takes a term with an extra variable in scope (σ ∷ Γ), and gives you a term without that variable in scope (Γ) but of type σ ⇒ τ10/02 03:33
copumpkinit might take a bit of mental contortions to see why that makes sense10/02 03:33
revenantphxI'm not even sure what to contort first >_<?10/02 03:33
copumpkinif I write (\x -> f x) z10/02 03:33
copumpkinit's saying that from the outside, the whole expression (\x -> f x) doesn't have x in scope10/02 03:34
copumpkinbut the (f x) inside it does have x in scope10/02 03:34
copumpkinfurthermore, (f x) has a type tau10/02 03:34
revenantphxright...10/02 03:34
copumpkinbut (\x -> f x) has type sigma -> tau, if x is of type sigma10/02 03:34
revenantphxAlright, that makes sense.10/02 03:35
copumpkinit's basically conveying all those statements in its type10/02 03:35
copumpkin  app : ∀ {σ τ Γ} → (f : Term Γ (σ ⇒ τ)) (x : Term Γ σ) → Term Γ τ10/02 03:35
copumpkinthat's taking a function and applying it to a value10/02 03:35
revenantphxlemme think about lam for a moment >_>10/02 03:35
copumpkinbasically saying if I have (a -> b) and (a), I can get b10/02 03:35
copumpkinsure :)10/02 03:35
revenantphxso going back to "lam is a constructor that takes a term with an extra variab..."10/02 03:36
copumpkinyep, sorry10/02 03:36
revenantphxcould you reiterate that?10/02 03:36
copumpkinsure10/02 03:36
revenantphxWhat's going in and coming out?10/02 03:36
copumpkinwhen I write (\x -> f x), the `lam` constructor would be taking a representation of that `f x`, and that `f x` needs to be able to see the x10/02 03:37
copumpkinso the lam is bringing x into scope for whoever it's wrapping10/02 03:37
copumpkin*whomever :P10/02 03:37
copumpkinin the type of lam10/02 03:38
revenantphxer... right. >_<...10/02 03:38
copumpkinthe sigma is the type of the x bound by (\x -> ...)10/02 03:38
copumpkinthe tau is the type of the ...10/02 03:38
revenantphxRight right ,I get that.10/02 03:38
copumpkinokay, sorry :)10/02 03:38
revenantphxi just don't get the code itself I suppose.10/02 03:38
RichardOWhat does σ ∷ Γ in Term (σ ∷ Γ) τ represent?10/02 03:38
revenantphx(sorry if I'm frustrating you)10/02 03:38
djahandarieThe new context10/02 03:38
revenantphxcons apparently.10/02 03:38
copumpkinRichardO: adding another type to the context10/02 03:38
djahandarieWhich you get by adding sigma to the old context10/02 03:39
copumpkinrevenantphx: not at all10/02 03:39
RichardOSo in lam you are taking σ out of the context?10/02 03:39
copumpkinit's taking any term that has sigma in context, and taking it out10/02 03:39
copumpkinyeah10/02 03:39
copumpkinwhich can be seen from the other side as the lam introducing the sigma for the enclosed operation10/02 03:39
copumpkinenclosed expression, I mean10/02 03:39
* djahandarie thinks that using the words new and old probably wasn't the best idea here10/02 03:39
revenantphxI guess one thing that's confusing me somewhat,10/02 03:40
revenantphxis that these just seem to be the types10/02 03:40
RichardOSorry using a list as the context representation is a little weird, but it makes sense10/02 03:40
revenantphxI'm really just not used to the langauge.10/02 03:40
revenantphxI only vaguely get the code.10/02 03:40
copumpkinrevenantphx: yeah, they are all just types10/02 03:40
copumpkinrevenantphx: that's what I meant by this not actually "doing anything"10/02 03:40
copumpkinI'm just defining a representation for my language10/02 03:40
revenantphxOh, ok. >_>10/02 03:41
copumpkinthe actual evaluation of the language is pretty straightforward10/02 03:41
revenantphxthat helps.10/02 03:41
copumpkinthe representation is designed to be very typesafe10/02 03:41
revenantphxaaaaah, now I see >_<10/02 03:41
copumpkinso I can't go constructing something like (\x -> x) x10/02 03:41
revenantphxright. right.10/02 03:41
copumpkinbecause x isn't in scope outside10/02 03:41
revenantphxokay then10/02 03:41
copumpkinand it also prevents me from using a given variable in badly typed ways within the language10/02 03:42
copumpkinRichardO: a lambda calculus with a more interesting type system would have something stronger than a list10/02 03:42
RichardOWould they use a set?10/02 03:42
copumpkinI wouldn't10/02 03:42
djahandarieWouldn't it just be a list of more interesting things?10/02 03:43
copumpkindjahandarie: they might depend on one another or be polymorphic10/02 03:43
copumpkinRichardO: the nice thing about a list is that I can still index into it with my variables, so I can keep track of what type each variable has easily10/02 03:43
djahandarieNow how do you make it dependent on the values? :P10/02 03:43
copumpkindjahandarie: conor has a crazy contortion for how to do that in agda10/02 03:44
djahandarieLink?10/02 03:44
copumpkindjahandarie: but even with a polymorphic lambda calculus, it starts getting pretty hairy10/02 03:44
djahandarieYeah I imagine10/02 03:44
copumpkinI can't remember, hmm10/02 03:44
copumpkindepnobby maybe10/02 03:44
copumpkinthere was another one though10/02 03:44
copumpkinhttp://personal.cis.strath.ac.uk/~conor/fooling/DepNobby.agda10/02 03:44
djahandarieWell that is something10/02 03:44
djahandarieYeah, found it10/02 03:44
* djahandarie goes back to setting up a proper agda environment10/02 03:45
copumpkinrevenantphx: anyway   either : ∀ {σ τ ρ Γ} → (f : Term (σ ∷ Γ) ρ) → (g : Term (τ ∷ Γ) ρ) → (x : Term Γ (σ + τ)) → Term Γ ρ10/02 03:45
copumpkinthat's pretty close to10/02 03:45
copumpkin:t either10/02 03:45
lambdabotforall a c b. (a -> c) -> (b -> c) -> Either a b -> c10/02 03:45
revenantphxone moment.10/02 03:45
copumpkinsorry :)10/02 03:45
revenantphxI got distracted ,reading backlog really quick.10/02 03:45
revenantphxlambdabot is in here too?10/02 03:46
revenantphxXD10/02 03:46
copumpkin:P10/02 03:46
copumpkinlambdabot is ubiquitous10/02 03:46
djahandarieIs it technically possibly to define Agda in itself?10/02 03:46
djahandarieWouldn't that be like proving a Set theory in itself?10/02 03:46
djahandarieIncompletness theorem10/02 03:47
copumpkinyeah, it shouldn't be possible10/02 03:47
copumpkinbut you can get close10/02 03:47
djahandarieI wonder what you lose10/02 03:47
copumpkinwell, you can write it in itself if you're satisfied with not using its own type system to represent its own type system10/02 03:47
djahandarieBut then there wouldn't be much point in writing in Agda would there?10/02 03:48
copumpkinwell, you could still prove things about it10/02 03:48
copumpkinso it would be valuable, I think10/02 03:48
RichardOThe analog to haskell's either would be either (lam a) (lam b) x?10/02 03:48
copumpkinRichardO: lam goes the wrong way, really10/02 03:48
copumpkinit's just either a b x where a and b are what you'd pass to lam in some representation of haskell :P10/02 03:49
revenantphxok so then back to either I suppose.10/02 03:49
copumpkinrevenantphx: the either constructor is basically a 2-ary lam10/02 03:49
revenantphxyeah thats what I was seeing10/02 03:49
revenantphxwith the cons'ing10/02 03:49
RichardOcopumpkin: woah, that just blew my mind10/02 03:49
copumpkinexcept it's also taking an Either to take apart10/02 03:49
copumpkinit could be structured in other ways, too10/02 03:50
revenantphxbut... it's taking 3 parameters?10/02 03:50
revenantphxheh?10/02 03:50
copumpkinit takes two "functions" (expressions with an additional bound variable) and the Either value to take apart10/02 03:50
copumpkinit's maybe not as elegant as it could be10/02 03:50
copumpkinit could take two actual functions of the => type10/02 03:50
* djahandarie doesn't see the connection to lam, as he would expect => to be used10/02 03:51
revenantphxOk, I don't quite get that,10/02 03:51
revenantphxwhy is it taking two functions?10/02 03:51
copumpkin:t either10/02 03:51
lambdabotforall a c b. (a -> c) -> (b -> c) -> Either a b -> c10/02 03:51
copumpkinone function is applied to whatever is in the Left case, and the other is applied to whatever's in the Right case10/02 03:51
copumpkin@src either10/02 03:51
lambdaboteither f _ (Left x)     =  f x10/02 03:51
lambdaboteither _ g (Right y)    =  g y10/02 03:51
revenantphxah, alright.10/02 03:51
revenantphxI see.10/02 03:51
copumpkinso it's basically just giving you a way of taking apart an Either that you're handed10/02 03:51
copumpkinit amounts to building either in as a primitive language construct, in the imaginary language I'm defining here10/02 03:52
copumpkinit's not very elegant, but you need _some_ way of taking it apart somehow10/02 03:52
revenantphxslowly but surely stuff is making more sense, don't worry :)10/02 03:52
copumpkincool :)10/02 03:52
revenantphxI thnk the biggest barrier is the language tbh.10/02 03:52
copumpkinyeah10/02 03:52
copumpkinI've written almost exactly this in Haskell too10/02 03:53
copumpkinbut my code tends to be ephemeral10/02 03:53
djahandarieWhy not exactly?10/02 03:53
djahandarie(Sans syntax)10/02 03:53
copumpkinwell, here the Type constructors are at the value level10/02 03:53
copumpkinin haskell I'm using actual types10/02 03:53
djahandarieAh, right10/02 03:53
copumpkinbut it's still possible10/02 03:53
copumpkininstead of list, I use nested tuples10/02 03:53
copumpkin(for the context)10/02 03:53
djahandarieHList to the rescue10/02 03:53
copumpkinHlist is a lot of baggage :)10/02 03:54
copumpkinI tend to just redefine what I need when I need it10/02 03:54
RichardOIs there a way to add back into a context?10/02 03:54
copumpkinindexing into it is pretty simple10/02 03:54
copumpkinRichardO: how do you mean?10/02 03:54
RichardOLike Term T x -> *magic* -> Term (a::T) x10/02 03:55
revenantphxhm10/02 03:55
copumpkinRichardO: yeah, just use a variable10/02 03:55
copumpkin  var : ∀ {τ Γ} → Var Γ τ → Term Γ τ10/02 03:56
RichardOfree variable?10/02 03:56
copumpkinsure10/02 03:56
copumpkinas you wrap it in binders it becomes progressively less free10/02 03:57
copumpkinbinders like lam or either10/02 03:57
copumpkineach binder steals one free variable10/02 03:57
RichardOAhh, I think that makes sense10/02 03:57
copumpkinrevenantphx: ready for app?10/02 03:57
copumpkinit's way simpler10/02 03:57
revenantphxsure10/02 03:57
copumpkin  app : ∀ {σ τ Γ} → (f : Term Γ (σ ⇒ τ)) (x : Term Γ σ) → Term Γ τ10/02 03:57
copumpkingiven a term of type (σ ⇒ τ) and a term of type σ, it gives you a term of type τ10/02 03:58
revenantphxI actually think I get that one off the bat.10/02 03:58
copumpkin:)10/02 03:58
revenantphxYeah, makes sense :P10/02 03:58
copumpkin_,_ and proj1 and proj2 are pretty straightforward10/02 03:58
copumpkin_,_ pairs up two terms into a _x_ type10/02 03:58
copumpkinproj1 and proj2 are like Haskell's fst and snd10/02 03:58
copumpkinthey take a _x_ type and pull out the two components10/02 03:59
copumpkin(proj for projection)10/02 03:59
djahandarieI think it's worth noting that you don't need inj,either, or (,),proj to have an untyped lambda calculus. They just exist to let you mess with sum times and product types, respectively (which are required for a typed lc)10/02 04:00
djahandarieBut this would be simpler in other places too if it wasn't typed10/02 04:00
revenantphxmmk...10/02 04:01
copumpkinyeah, and the usual simply typed lambda calculus doesn't include sums and products either10/02 04:01
copumpkinit just means you can't actually do anything with it10/02 04:01
revenantphx:)10/02 04:01
copumpkinthe usual presentation of the STLC just has _=>_ and 1#10/02 04:01
djahandarieYou should probably explain Var right now to tie things together btw :P10/02 04:02
copumpkinyeah10/02 04:02
RichardOIs there any interesting research with lambda calculus that deals with non-algebraic datatypes?10/02 04:02
djahandarie(In case you forgot about it... :P)10/02 04:02
copumpkinnope, I hadn't :)10/02 04:02
copumpkinso, data Var : Context → Type → Set where10/02 04:02
copumpkinit has a context and a type like Term10/02 04:02
copumpkinsame "shape"10/02 04:03
revenantphxmm10/02 04:03
copumpkinevery variable has a type, and exists within a context10/02 04:03
revenantphxright10/02 04:03
copumpkinso   zero : ∀ {τ Γ} → Var (τ ∷ Γ) τ10/02 04:03
copumpkinthat means forall types tau and contexts gamma, zero is a variable with an additional type in context (tau) and the variable has type tau10/02 04:04
copumpkinit's basically tying itself to the head of the list10/02 04:04
revenantphxk10/02 04:04
copumpkinon the other hand,   suc  : ∀ {σ τ Γ} → (n : Var Γ τ) → Var (σ ∷ Γ) τ10/02 04:05
copumpkinit takes another variable index with context gamma and type tau, and returns a variable with an unrelated type sigma stuck onto the context, and the same type tau10/02 04:06
copumpkinit may not be very obvious why this is useful :P10/02 04:06
revenantphxhm yeah10/02 04:06
revenantphxlooking at that one a bit10/02 04:06
revenantphxexplain?10/02 04:06
RichardOConstructors add to the context10/02 04:06
copumpkinrevenantphx: trying to think of a good way of illustrating this10/02 04:08
revenantphxmmk10/02 04:08
copumpkinso10/02 04:08
copumpkinsay you have some context [y, z], and you enter a lambda10/02 04:09
copumpkinthe lambda is sticking an x onto the front of that list10/02 04:09
copumpkinso you get an [x, y, z]10/02 04:09
copumpkinright?10/02 04:09
revenantphxright10/02 04:09
copumpkinnow, the zero constructor of Var says that for _all_ gammas, it'll give you a Var (τ ∷ Γ) τ10/02 04:10
copumpkinso if you use zero here, tau will magically be x10/02 04:10
copumpkinjust by unifying the two things10/02 04:10
revenantphx...one moment10/02 04:10
revenantphxI've got a phone call10/02 04:10
copumpkinsince tau unifies with x and gamma unifies with [y, z]10/02 04:10
copumpkinsure10/02 04:10
revenantphxalright back10/02 04:13
copumpkindo you see what I'm saying about unifying the (τ ∷ Γ) with [x,y,z] ?10/02 04:15
copumpkinwhere [x,y,z] means x ∷ (y ∷ (y ∷ []))10/02 04:15
revenantphxer yeah10/02 04:15
revenantphxjust like pattern matching10/02 04:16
copumpkinsort of10/02 04:16
copumpkinit's closer to what you get in types in haskell10/02 04:16
djahandarieImportant to note that x y and z here are types, not names10/02 04:16
revenantphxah, right10/02 04:16
copumpkinyeah10/02 04:16
copumpkinso if I'm in a context [x,y,z]10/02 04:17
copumpkinand I use var zero, I'll magically have a Term of type x10/02 04:17
copumpkinbecause of how that unifies10/02 04:17
revenantphxMmk...10/02 04:17
copumpkinthe type of suc is saying that I can prepend additional crap to my context and still retain my type10/02 04:18
copumpkinso if I use suc zero on that context, I'll get a Var of type y, and the random crap that suc adds on is the x10/02 04:18
revenantphxRight.10/02 04:18
revenantphxso succ won't change the type?10/02 04:19
copumpkinnope, it lets you reach into the context and retrieve something that isn't at the head10/02 04:19
revenantphxor rather, it will jsut append the same type again10/02 04:19
revenantphx?... hrm10/02 04:19
lambdabotNot enough arguments to @.10/02 04:19
revenantphxit looks to me like its just appending some random crap the context.10/02 04:21
RichardOzero doesn't take any arguments. How does it know what context to use?10/02 04:21
revenantphxNot seeing anything else >_<.10/02 04:21
revenantphxRichardO: Also, yeah that.10/02 04:21
djahandarieType unification.10/02 04:21
copumpkinRichardO: unification with wherever it's used10/02 04:21
revenantphx0.o10/02 04:21
revenantphxMore type system magic?10/02 04:22
djahandarieHappens in Haskell too.10/02 04:22
djahandarieYou have two types, now try to put them together. That is unification10/02 04:22
revenantphxdefine "put them together" :P10/02 04:22
copumpkinif I have Either a Int and Either Bool b, and I try to unify them, the unification of them is Either Bool Int10/02 04:22
djahandarieIt either fails, or makes the more general of the two types more specific.10/02 04:22
revenantphxcopumpkin: ah okay10/02 04:23
revenantphxso it can infer the type by unifying the partially specified/inferred/w.e ones?10/02 04:23
copumpkinyeah10/02 04:24
djahandarieHow do I still not have an Agda enviornment set up after an hour. Keep on getting distracted. :P10/02 04:24
revenantphxokay then10/02 04:25
revenantphxso I think I get the gist of the stuff :\10/02 04:25
revenantphxso which subset of this would go into the most simple STLC possible?10/02 04:26
revenantphxand tbh, is it even really reasonable to generate llvm for it XD?10/02 04:26
revenantphxIt can't *do anything*.10/02 04:26
djahandarieThe top two blocks don't do anything. The bottom one does.10/02 04:26
djahandarie(When added on.)10/02 04:26
copumpkinrevenantphx: I wouldn't compile the pure STLC to llvm10/02 04:27
copumpkinbut something like this could actually do something10/02 04:27
copumpkinif you add the bits at the bottom, as djahandarie said10/02 04:27
revenantphxSeems more useful for parsing/lexing exercise.10/02 04:27
copumpkinI'd normally leave that shit out :P10/02 04:27
revenantphxI mean, it seems like it would be non-trivially annoying/useless to output as LLVM10/02 04:27
copumpkinI don't really care about surface syntax10/02 04:28
djahandarieOops, there were three blocks of code on the top. Four total. :P10/02 04:28
RichardOCould you use zero and suc in an example?10/02 04:28
copumpkinsure10/02 04:28
copumpkinlet's see10/02 04:30
copumpkinhow about10/02 04:30
copumpkinsorry, just eating :P10/02 04:31
djahandarieEating dinner at 11:30? lol10/02 04:31
copumpkinI have pretty weird schedules10/02 04:32
djahandarieI want to somehow get Agda on my laptop so I have something to do tomorrow in my useless Discrete Systems class.10/02 04:33
djahandarieAny way to get Agda without compiling it? :P10/02 04:33
copumpkinget someone else to compile it for you :P10/02 04:33
copumpkinunfortunately I don't have a working copy of it either right now10/02 04:33
djahandarieI have it compiled on my desktop10/02 04:33
djahandarieBut it was done by cabal so I have no idea what is where10/02 04:33
copumpkinah10/02 04:34
djahandarieCould build it from darcs then just slap all that stuff onto the laptop. Oh well, too much :effort: at midnight anyways. :P10/02 04:35
revenantphxthanks copumpkin10/02 04:40
revenantphxI'm going to go to sleep i na sec10/02 04:40
revenantphxI appreciate the help10/02 04:40
copumpkinah okay10/02 04:40
copumpkinno problem10/02 04:40
revenantphxif you could leave that up that'd be nice btw10/02 04:41
copumpkinRichardO: I'll work through how zero and suc work in a few, when I finish eating10/02 04:41
copumpkinrevenantphx: oh yeah, it's been up for months now :)10/02 04:41
revenantphxwonderful10/02 04:41
RichardOk, no prob10/02 04:41
copumpkinman, I really wish I had agda to compute these types for me :P10/02 04:53
lambdabotcopumpkin: You have 1 new message. '/msg lambdabot @messages' to read it.10/02 04:53
copumpkinRichardO: maybe it'd be best for you to load that code into agda10/02 04:53
copumpkinand put holes in strategic places and see what's what10/02 04:53
copumpkinunless you don't have agda installed10/02 04:53
RichardOwould coq work?10/02 04:53
copumpkinactually, let me translate it to haskell really quickly10/02 04:53
djahandarieRichardO, putting Agda code in Coq will not work. :P10/02 04:54
RichardOdjahandarie: haha, wouldn't that be something10/02 04:55
copumpkinRichardO: here it is in Haskell: http://hpaste.org/43836/stlc10/02 05:05
djahandarieNice10/02 05:05
RichardOhaha, the good ol' stlc10/02 05:05
djahandarieHaha at the comment10/02 05:06
copumpkin:)10/02 05:06
djahandarieIs there a way to do it without rank n types?10/02 05:06
copumpkinso let me do something here10/02 05:06
copumpkinI'm just using RankNTypes for the explicit forall syntax :P10/02 05:07
copumpkinto make it look closer to the agda10/02 05:07
djahandarieAh. Why not just existentialquantification or whatever that extension is10/02 05:07
copumpkinI picked one :P10/02 05:07
djahandarielol10/02 05:07
copumpkinplus I like RankNTypes and think it should be on by default10/02 05:07
djahandarieDoesn't it cause type inference issues past rank2?10/02 05:07
copumpkinit just can't be inferred at all10/02 05:07
copumpkinbut who cares :P10/02 05:08
djahandarielol10/02 05:08
copumpkinI guess people like haskell to be able to infer the most general type of any expression10/02 05:08
copumpkinand rankntypes means there's a more general one that won't get inferred, in some cases10/02 05:08
djahandarieWhy can't we just have some magical type inference thing10/02 05:08
djahandarieHindley-Milner is too fragile!10/02 05:09
RichardOAhh, so you can represent x and y with Var Zero and Var (Suc Zero). If we have z we could arbitrarily represent z with Var (Suc (Suc Zero))10/02 05:09
copumpkinyeah, depending on where it got bound of course10/02 05:09
RichardOoh ok, it's not arbitrary10/02 05:10
RichardOit relates to the lam's10/02 05:11
copumpkinyep10/02 05:11
copumpkineach one shifts the existing ones over by one10/02 05:11
copumpkinhttp://hpaste.org/paste/43836/stlc_clearer#p4383710/02 05:11
copumpkinthat one might be easier to read10/02 05:12
djahandarieTypeOperators should be on by default10/02 05:12
djahandarieIt doesn't cause any inference issues afaik ;)10/02 05:12
copumpkinhttp://hpaste.org/paste/43836/stlc_less_noise#p4383810/02 05:13
copumpkinthat's less noise10/02 05:13
copumpkinlol10/02 05:13
RichardOThe way type unification works backwards is alittle weird.10/02 05:13
copumpkinit works in all sorts of directions!10/02 05:13
copumpkin:P10/02 05:13
djahandarieDoes it work in 3D?!10/02 05:13
copumpkinhere, let me illustrate how the types work in this example10/02 05:14
copumpkinRichardO: http://hpaste.org/paste/43836/stlc_annotation#p4383910/02 05:20
copumpkinRichardO: note that if I replace test0's definition in there (flipping the variables) with test0 = Lam (Lam (App (Var (Suc Zero)) (Var Zero)))10/02 05:21
copumpkinit breaks the type10/02 05:21
copumpkinbecause (\x -> (\y -> x y)) has a different type from (\x -> (\y -> y x))10/02 05:21
copumpkinI suppose there was a smarter order to take those holes out, but meh :)10/02 05:22
RichardOtest6 actually explains alot.10/02 05:25
RichardOtest6 hole type could also be written Term (s, ((s :=> t), g)) t, right?10/02 05:31
RichardOwait, no Term ((s :=> t), (s, g)) t10/02 05:32
copumpkinyep, sorry10/02 05:34
copumpkinGHC just inferred that more general type on it10/02 05:34
RichardOWhat is g?10/02 05:35
RichardOis it the 'empty context'?10/02 05:36
copumpkinit's any context10/02 05:36
copumpkindoing it this way allows this to be embedded in other expressions with bound variables (and it just won't mention those variables)10/02 05:36
copumpkinyou'll notice that in my original agda code, the actual evaluator can only run expressions with an empty context10/02 05:37
copumpkinmeaning that it's a fully closed expression, with no unbound variables in it10/02 05:37
copumpkinI can write the evaluator on the haskell side too if you're interested10/02 05:38
RichardODoes this page kinda cover all the stuff you've been talking about?10/02 05:41
RichardOhttp://www.seas.upenn.edu/~cis500/current/sf/html/Stlc.html10/02 05:41
copumpkinyeah, except it's more explicit10/02 05:42
copumpkinand their STLC just has bools and naturals in it10/02 05:42
copumpkinbools I can represent easily as 1 + 1, but naturals I can't represent at all in mine :P10/02 05:43
copumpkinso their "AST" (tm) doesn't carry any type or context information, so they need to go proving stuff about it and stating things like the typing relation (has_type) by hand10/02 05:43
copumpkinas far as I can understand, it's because inductive families are less useful/powerful in coq than they are in agda, but it may just be a different approach to representing problems10/02 05:44
copumpkinthey have fancy tactics that do a lot of the work we have to do by hand for them10/02 05:45
copumpkinso we try to come up with nice ways to avoid doing that work by encoding invariants in our types10/02 05:45
* copumpkin shrugs10/02 05:45
copumpkinI really haven't used coq much beyond the basic stuff10/02 05:45
copumpkinI read chlipala's and that's the extent of my knowledge about it :P10/02 05:45
RichardOYea, once I got to this page, the tactics became too much like magic. It became harder to know what was actually going on.10/02 05:46
RichardOI haven't tried proving things with agda, yet.10/02 05:47
copumpkinin agda proving is writing expressions and pattern matching, but they'll often have tricky types and will take some thought to figure out what you're allowed to put where (luckily it can help you along automatically)10/02 05:48
copumpkinI guess the approach in the page you linked to lets them put in stranger typing rules10/02 05:49
copumpkinand have it break other things10/02 05:50
RichardOOne thing I noticed about agda that made me weary was that the types can look like a perl one liner.10/02 05:51
RichardOWould it make sense to have the equivalent of a 'let expression' in the type signature?10/02 05:51
copumpkinfor what? to give things names?10/02 05:52
copumpkinor are you talking about the equivalent of lam in the type language?10/02 05:52
RichardOYea, I guess a local scope for names.10/02 05:52
copumpkinyeah, that starts taking you in the direction of polymorphic types and fancier typing stuff10/02 05:53
copumpkinthere's a lot of fun to be had there10/02 05:54
copumpkinin the haskell type "forall x. [x]", the forall is really a type-level lambda10/02 05:55
copumpkinso it's basically (\x -> [x])10/02 05:55
copumpkinan instantiation of that type to [Int] is type-level application of the lambda to Int10/02 05:55
copumpkinin fact, GHC's core language represents these lambdas and applications explicitly10/02 05:56
RichardOInteresting. Seems that it only allows for a "point-free" way of dealing with types10/02 05:56
copumpkinhow so?10/02 05:57
RichardOhmm, maybe point-free isn't the word I'm looking for10/02 05:59
RichardOit's hard to do this:10/02 06:01
RichardOf x = x + 110/02 06:01
RichardOf :: a -> a where a = Int10/02 06:01
RichardOor something like that10/02 06:01
copumpkinoh, yeah, you could have a construct for creating explicit bindings like that10/02 06:02
copumpkinfor sharing and such10/02 06:02
copumpkinand you could have it on the type level and value level10/02 06:02
RichardOright10/02 06:02
copumpkincan you think of what the constructor for the let binding would look like given the agda or haskell versions of STLC I put up earlier?10/02 06:03
RichardOObviously for most Haskell types, it's pretty useless. But I wonder if it could make Agda types easier to read.10/02 06:03
copumpkinin agda you can actually use let x = y in x in types, since types are just expressions like anything else :)10/02 06:04
RichardOoh, I've never seen that syntax used.10/02 06:04
copumpkinyeah, I'm not sure it's very common10/02 06:04
copumpkinbut yeah, you can write functions that compute types for other functions10/02 06:05
copumpkinsometimes you may even need to jump through hoops to prove that a type can be constructed, and then jump through more hoops to construct the value of such a type :)10/02 06:05
copumpkinbut a common example is the type of printf10/02 06:06
copumpkinwhere you'd have PrintfType : String -> Set; and printf : (fmt : String) -> PrintfType fmt10/02 06:06
copumpkinwhere PrintfType parses the format string and constructs the resulting function type for it, and then printf actually interpolates the values into the format string10/02 06:07
RichardOIt's crazy that printf's type can change how it is parsed10/02 06:07
copumpkinyou mean how the format string can affect its type?10/02 06:07
RichardOIf the format string is unknown, then it can't be parsed.10/02 06:08
copumpkinoh yeah10/02 06:09
RichardOYou don't know how many arguments printf takes.10/02 06:09
copumpkinyeah10/02 06:09
copumpkinthe typical approach is to make it expect a value of the empty type if the format string is invalid, I think10/02 06:09
RichardOIs the let binding App (Lam (Var Zero)) or something?10/02 06:18
copumpkinyou could implement it that way: Let f x = App (Lam f) x10/02 06:20
RichardOIs there a difference in our definitions?10/02 06:23
copumpkinyours is id10/02 06:24
copumpkinLam (Var Zero is (\x -> x)10/02 06:25
RichardOhmmm, why does Let f x feel the same as App f x10/02 06:26
RichardOOh wait, lam is creating a new variable?10/02 06:27
copumpkinlet x = y in T x ~ (\x -> T x) y10/02 06:27
copumpkinyeah, or is binding one at least10/02 06:28
RichardOThat's cool. Thank god type inference can do most of this for us.10/02 06:33
copumpkin:) yep10/02 06:36
RichardOLet : Term g (b :=> a) -> Term (a, g) b -> Term g a?10/02 06:39
RichardOhmmm, i'm about 90% sure i'm wrong10/02 06:40
copumpkinI'd do it as Let : Term (t, g) s -> Term g t -> Term g s10/02 06:42
RichardOLet : Term (a, g) b -> Term g b -> Term g a10/02 06:42
copumpkinthat's a tiny bit backwards10/02 06:42
RichardOah, right10/02 06:42
RichardOMy brain keeps switching between being heavily confused and enlightened.10/02 06:46
RichardOI should probably get some sleep.10/02 06:46
copumpkinyeah :)10/02 06:47
RichardOThanks for the help!!10/02 06:47
copumpkinnp10/02 06:47
djahandariecopumpkin, how do I do djinn type stuff in Agda?10/02 16:58
copumpkinC-c C-a can do some of that10/02 16:58
copumpkinin a hole10/02 16:58
djahandarieHow powerful is it?10/02 16:58
copumpkinit's hard to say10/02 16:59
djahandarieCan it work with an inductive type?10/02 16:59
copumpkinI use it quite often10/02 16:59
copumpkinto fill in things I can't be bothered to type out, but are obvious how to solve10/02 16:59
copumpkinif they're really obvious, you can just write in _10/02 16:59
copumpkinbut C-c C-a is more powerful than _10/02 16:59
djahandarieWhat is _?10/02 17:00
copumpkinit just means "infer"10/02 17:00
copumpkinand by "infer" I mean unify10/02 17:00
copumpkinif the context uniquely determines what could fit in there10/02 17:00
copumpkinthen _ will work and won't be yellow10/02 17:00
copumpkinyou can write _ anywhere10/02 17:00
copumpkinbut it'll turn yellow in most places10/02 17:00
dolioIt's a very strict requirement of obviousness, too.10/02 17:04
dolioFor instance it isn't "obvious" that for "data Top : Set where tt : Top", tt is the only inhabitant.10/02 17:05
copumpkinbut if you switch data to record, it will be (with the correct syntax for the constructor)10/02 17:11
copumpkindjahandarie: so I take it you have a working install of it now?10/02 17:11
djahandarieNope. :< On my laptop right now10/02 17:11
copumpkinoh10/02 17:11
dolioYes, record Top is "obvious" because all elements are eta expanded into 'record{}'.10/02 17:23
copumpkinpeople seem to make a big deal about that thing10/02 17:24
dolioI think the only other sort of thing that's obvious is the type of an expression.10/02 17:24
dolioExcept, of course, expressions like (x, y) whose types are under-determined.10/02 17:25
dolioAnd of course, relying on that obviousness will bite you if you start fiddling with universes.10/02 17:26
dolioBecause expressions having obviously unique(ish) types doesn't translate into them having obviously unique universe codes.10/02 17:27
copumpkinI've been thinking10/02 17:28
copumpkinI'd really like Haskell's view pattern syntax in Agda10/02 17:28
copumpkinwith is rather syntactically heavy sometimes10/02 17:28
dolioI suspect it's a somewhat more tricky proposition in Agda.10/02 17:34
doliofoo m (compare m -> gt k n) ...10/02 17:35
doliom needs to be refined to n + suc k.10/02 17:35
copumpkinhow would it be any different than a with block?10/02 17:35
copumpkinoh10/02 17:36
copumpkinso just the refinements I'd have to write out by hand in the with block because it can't figure them out?10/02 17:36
dolioWell, I mean, what would that line look like refined?10/02 17:37
doliofoo .(n + suc k) (compare (n + suc k) -> gt k n) ...?10/02 17:37
dolioThat's weird.10/02 17:37
copumpkinwell, I meant desugaring it to10/02 17:37
copumpkinfoo m q with compare m10/02 17:37
copumpkin... | gt k n = ...10/02 17:38
copumpkinand I guess punting when the refinements get too complicated :P10/02 17:38
copumpkinI mean compare m q10/02 17:38
dolioSure, you could just say, "this is too dependent for view patterns."10/02 17:38
copumpkinclearly a very elegant proposal :)10/02 17:38
dolio:)10/02 17:39
* copumpkin goes back to the drawing board10/02 17:39
dolioOn the upside, there could be an error message like, "my brain just exploded."10/02 17:40
copumpkinI'd take that10/02 17:41
copumpkinI guess even the embmax view on Fin n would be too complicated for it though10/02 17:41
dolioI don't remember what that is.10/02 17:42
dolioThe ironic part would be, a lot of what are actually called "views" might be too fancy to work well.10/02 17:43
copumpkinyeah10/02 17:43
copumpkinthe embmax one says that either a Fin is the max of its range or it's embeddable in a smaller Fin10/02 17:43
dolioAh, okay.10/02 17:44
dolioWell, I think if your viewing function is like '(x : A) -> V x', where V doesn't have any other relevant indices, it might be okay.10/02 17:45
copumpkin_and_ your viewing function doesn't refer to other pattern-bound variables?10/02 17:46
dolioThe obvious problem with compare m is that it's (n : Nat) -> C m n.10/02 17:46
dolioSo it can refine m, as well.10/02 17:46
copumpkinyeah10/02 17:47
copumpkinit could silently refine m and then if you ever tried to use m, it'd complain that it was refined elsewhere10/02 17:47
copumpkinseems ugly though10/02 17:47
copumpkinit'd sort of be "linear types" on the pattern-bound variable, if it's used in a view pattern that refines it10/02 17:47
copumpkinnot sure if that makes any sense10/02 17:48
copumpkinaw10/02 17:48
dolioAnyhow, maybe you should just go use Epigram 1 for a while. Even structural recursion has syntax like a with there (because, I think, it all uses a common facility).10/02 17:51
copumpkinI see10/02 17:51
dolioThen you can come back and be refreshed by all the non-with things Agda allows you to do.10/02 17:51
copumpkinlol10/02 17:51
copumpkinI was just mentioning that it seems that any variables that are refined in types of view patterns should be treated linearly10/02 17:51
copumpkinor something10/02 17:51
copumpkinso you don't get to refer to them anymore10/02 17:52
dolioYeah, but linearly meaning that 'foo m ...' counts as a "use" of m?10/02 17:53
dolioSo you can't "use" it on the right hand of the equals sign?10/02 17:53
copumpkinwell, not quite10/02 17:53
copumpkinonly if the "use" of it results in it appearing as an index of an inductive family resulting from a view pattern :P10/02 17:54
dolioOh, or the "compare m" counts as a use?10/02 17:54
copumpkinbasically "yo, I'm sorry man but I can't let you touch that m. It was tainted by your view pattern"10/02 17:54
dolioThe "compare m" counting as a use would be more typical, I think.10/02 17:54
copumpkinyeah, that'd probably be simpler10/02 17:55
dolioSince it sort of is on the expression side of things.10/02 17:55
dolioAnyhow, that might work. Seems complicated, though.10/02 17:55
copumpkinyeah, a lot more complicated than the simple syntax + desugaring I was originally thinking of10/02 17:56
dolioIt might be hard to tell what qualifies for your criterion.10/02 17:56
dolioWhat counts as an index of an inductive family.10/02 17:56
copumpkinanything to the right of that :10/02 17:57
copumpkinif you use those like parameters, then it's your fault10/02 17:57
doliodata Foo (x : A) : Set where foo : TrickedYa x -> Foo x10/02 17:57
copumpkinlol10/02 17:57
doliodata TrickedYa : A -> Set where ...10/02 17:57
copumpkinokay fine10/02 17:57
copumpkinif it's anywhere in the applied type constructor of the result of your view pattern?10/02 17:58
dolioThat's probably safest.10/02 17:58
dolioOf course, maybe there's problems with that that I'm not imagining.10/02 17:58
copumpkinprobably :/10/02 18:01
copumpkinI wonder what problems allowing that ridiculous inductive family I came up with a while back would lead to10/02 18:01
copumpkinthe variable-arity inductive family10/02 18:01
dolioOh, yeah.10/02 18:01
dolioTo be honest, I'm kind of glad that isn't allowed, too. :)10/02 18:02
copumpkin:(10/02 18:02
dolioIt's possible it can be encoded by other means, though. Just not as an inductive family.10/02 18:02
copumpkinyeah, I'm sure10/02 18:02
copumpkinit could probably be done with the usual existential + equality thing10/02 18:03
dolioI don't think the variable arity fits with the underlying justification of inductive families, though.10/02 18:04
dolioThe idea being that F(i) is a set/type you're defining by induction.10/02 18:07
dolioInitial algebras in the category of I-indexed types.10/02 18:07
dolioBut your variable arity thing isn't a type for all i.10/02 18:08
dolioWhat it is depends on i.10/02 18:08
copumpkinyeah10/02 18:09
copumpkinwell, aren't fibrations usually used to model those evil dependent functions? couldn't that definition of inductive families be extended in a similar way?10/02 18:10
* copumpkin 's knowledge stops short of that stuff10/02 18:10
copumpkinoh, the ncatlab article on it is actually vaguely comprehensible10/02 18:12
copumpkinsome parts of it, anyway10/02 18:12
dolioI-indexed families are objects fibred over I.10/02 18:12
copumpkinyeah, but this would be "doubly fibered" or something!10/02 18:13
dolioMost of the categorical type theory I've seen doesn't model I -> Set kind of stuff directly.10/02 18:13
copumpkinah :(10/02 18:13
dolioAnyhow, my description above makes me think: we need to inspect i prior to doing stuff with F(i).10/02 18:15
dolioBecause what F(i) is is probably defined by recursion on i.10/02 18:15
dolioFor instance, it may not (probably doesn't) even make sense to write: (i : I) -> F i10/02 18:16
copumpkinyou mean like my evil example?10/02 18:17
dolioWell, for some i, F would only be partially applied there, right?10/02 18:17
copumpkinI guess it doesn't even know what sort the base case would be at that point10/02 18:17
dolioIt'd need to instead be (i : I) (j : J) -> F i j10/02 18:17
copumpkinoh, F takes two parameters10/02 18:18
dolioHow many parameters it takes is variable, right?10/02 18:18
dolioDepending on i.10/02 18:18
copumpkinoh, not that way10/02 18:19
copumpkinalthough that's even more of a mindfuck10/02 18:19
dolioApparently I don't remember what your example was doing, then.10/02 18:21
copumpkinI meant something like10/02 18:21
copumpkinF : Nat -> Set10/02 18:21
copumpkinF 0 = Set10/02 18:21
copumpkinF (suc n) = Nat -> F n10/02 18:21
copumpkinthen data Evil : (n : Nat) -> F n where10/02 18:21
dolioOh, no, I got it right, I think.10/02 18:22
copumpkinwell, F doesn't take more than one argument10/02 18:22
dolioEvil 0 : Set Evil 1 : Nat -> Set, Evil 2 : Nat -> Nat -> Set10/02 18:22
copumpkinit results in a type of an n-ary function10/02 18:22
copumpkinyeah10/02 18:22
dolio(n : Nat) -> Evil n10/02 18:23
dolioProblem.10/02 18:23
copumpkinoh okay10/02 18:23
copumpkinyeah, that's the problem10/02 18:23
dolio(m n : Nat) -> Evil m n10/02 18:23
dolioProblem.10/02 18:23
copumpkinEvil (suc m) n?10/02 18:24
dolioHowever, F n ~ Vec Nat n -> Set, so you can get it that way.10/02 18:25
dolioSo there's your double fibration. :)10/02 18:26
copumpkinone could imagine an even more painful, dependent example of this though10/02 18:26
copumpkinwhere F n makes dependent functions :P10/02 18:26
copumpkinbut I guess those are equivalent to terrifying n-ary dependent pairs10/02 18:26
dolioYes. And then instead of Vec A you use telescopes or something.10/02 18:27
* copumpkin 's brain melts10/02 18:27
dolioAnyhow, for some reason, the curried version is much harder to use.10/02 18:32
dolioI guess because there's no way of abstracting over an arbitrary number of things, aside from indexed tuples like Vec.10/02 18:32
copumpkinyeah10/02 18:33
dolioAnd there's not much point in currying F if the only way you can use is it 'uncurry F v'.10/02 18:33
copumpkinclearly we need primitive support for n-ary functions10/02 18:34
dolioAlso not, in categorical type theory, when you go to model something like (i : I) -> J i -> Set, what you end up modeling is more like Sigma I J -> Set.10/02 18:34
dolioSo this isn't specific to your variable arity thing.10/02 18:34
copumpkinyeah, I see10/02 18:35
dolioWow, unit testing Agda with elisp. What a combination.10/02 19:11
copumpkindid you see his comment on reddit?10/02 19:12
dolioHe's unhappy that he spent the time on it. A common reaction to working with elisp, I think.10/02 19:12
copumpkinyeah10/02 19:13
glguy"Whaaaaat? Oh, FFS. I wish someone had told me this before I spent a week mucking about with elisp.10/02 19:31
glguyOh well, I guess I had fun and learned something."10/02 19:31
dolioPerhaps he can become an elite agda-mode hacker and add new, exciting functionality.10/02 19:33
copumpkinI'd quite like the ability to split on multiple parameters10/02 19:45
copumpkinunless someone already added that10/02 19:45
glguyI had a function Bool -> Bool -> Bool -> Bool where I wanted that10/02 19:45
glguytook forever :)10/02 19:45
copumpkinyeah10/02 19:46
copumpkinit'd also be nice if case splitting always built valid code10/02 19:46
dolioBerry's majority function?10/02 19:46
glguyI like having to go back and fix all of the mistakes that the case splitter made regarding implicit arguments and dot-patterns10/02 19:47
glguyit makes it exciting10/02 19:47
copumpkinlol10/02 19:47
copumpkinI guess that's a virtue10/02 19:47
dolioI enjoy it when the splitter thinks it has to break something over multiple lines, but doesn't know how to do it.10/02 19:47
glguyan alternate solution would be making the case splitter add the original as a comment for reference to make it easier to fix all of the mistakes it made10/02 19:48
copumpkinI enjoy it when the splitter renames variables I named so it can use those names instead of me10/02 19:48
dolioThat one, at least, probably isn't that hard to fix. Just, "make lines as long as you want."10/02 19:48
dolioYeah, it'd be nice if it tried to preserve the names that are already there.10/02 19:49
copumpkinhttp://www.mail-archive.com/epigram@durham.ac.uk/msg00229.html10/02 19:50
copumpkinis interesting10/02 19:50
dolioIf I case analyze on 'm', make the pattern 'suc m' instead of 'suc n', even though the Nat definition suggests otherwise.10/02 19:50
copumpkinwhat if suc took two parameters?10/02 19:50
dolioIt doesn't. Anyhow, it's just a preferable heuristic to what it does currently in quite a few cases.10/02 19:51
dolioThere's lots of interesting stuff on that old mailing list.10/02 19:53
dolioI recommend reading some Yong Luo vs. Conor McBride discussions.10/02 19:54
dolioIf you're into schadenfreude, that is.10/02 19:56
copumpkinlol ok10/02 19:57
doliohttp://www.mail-archive.com/epigram@durham.ac.uk/msg00231.html10/02 19:59
dolioThat's probably a good one.10/02 19:59
copumpkinI was just reading it :)10/02 19:59
copumpkinyeah, rather painful10/02 20:04
djahandarieWho is Yong Luo?10/02 20:11
copumpkinan ex researcher at kent, it seems10/02 20:11
copumpkinhttp://www.mail-archive.com/epigram@durham.ac.uk/msg00238.html10/02 20:11
copumpkinawkward :P10/02 20:11
djahandarieThat's what I found from researching too10/02 20:11
djahandarielol10/02 20:11
copumpkinwow10/02 20:12
copumpkinit got quite actively hostile10/02 20:12
djahandarieYeah10/02 20:13
djahandarieSeems like a language barrier10/02 20:13
dolioEpigram is like the wild west.10/02 20:13
djahandarie(At least partially)10/02 20:13
djahandariedolio, maybe the wild east in this case...10/02 20:13
copumpkindjahandarie: not at all, to me10/02 20:14
copumpkinhis english seems close to flawless, but he just ignores what conor has to say and repeats his original point10/02 20:15
dolioIt seems more like a crank type discussion.10/02 20:15
dolioAlthough, somewhat less cranky than your average crank topic.10/02 20:16
copumpkinyeah10/02 20:16
copumpkinmost cranks pick "pop math" that they misunderstand to refute10/02 20:16
* djahandarie doesn't know what crank means10/02 20:17
copumpkincrackpot10/02 20:17
dolioI HAVE REFUTED CANTOR!10/02 20:17
dolioGOEDEL WAS WRONG!10/02 20:17
copumpkindjahandarie: dolio is a crank10/02 20:18
djahandarieI see. :P10/02 20:18
djahandarieLike a troll that believes what they are saying?10/02 20:18
dolioYes.10/02 20:18
copumpkinpretty much10/02 20:18
djahandarie:(10/02 20:18
dolioI should have inserted something about how I am a lone, visionary genius, too.10/02 20:18
copumpkindjahandarie: you'd be amazed (or maybe not) at how many people "refute" cantor online10/02 20:19
copumpkindolio: and a spiral of reals centered around pi?10/02 20:19
djahandarieReminds of those stupid proofs people do that end up in 2=110/02 20:19
djahandarieWhich always involve dividing by 0 or something stupid10/02 20:19
dolioHave you heard about my plutonium atom totality theory?10/02 20:19
copumpkinooh10/02 20:19
djahandarieOh you mean the one where you discover the higgs boson? Yeah that was a good one10/02 20:20
dolioHeh, John Baez is on the page of "usenet celebrities" with Archimedes Plutonium.10/02 20:22
dolioThe wikipedia page.10/02 20:23
copumpkinugh, he's like a broken record10/02 20:23
dolioObviously for different reasons.10/02 20:23
copumpkinoh I was talking about yong10/02 20:24
copumpkinI wonder if he's related to zhoului, since they seem to share at least one paper10/02 20:24
copumpkinhui10/02 20:24
dolioDunno. Z. seems to be more on the ball.10/02 20:25
copumpkinindeed :P10/02 20:25
dolioAnd yeah, I think Yong only ever talks about that one topic, at least on that list.10/02 20:26
dolioKind of the same thing over and over.10/02 20:26
dolioOh, nope. Found him talking about something else.10/02 20:27
copumpkinthe coq matrix operation?10/02 20:27
dolioHe replied to someone about functor laws.10/02 20:27
copumpkinconor says in an unrelated thread "that definition of majority should be definable for the purpose of reasoning, but it's silly computationally. maybe we should decouple computation from reasoning" and yong responds "you can only solve this with partial functions"10/02 20:27
dolioHehehe.10/02 20:28
dolioAnyhow, the problem with reasoning about things like the majority function does come up once in a while.10/02 20:35
dolioAnd I'm not sure anyone has a good solution.10/02 20:35
copumpkinwas glguy actually trying to define it?10/02 20:36
copumpkinglguy: ? :)10/02 20:36
dolioI don't know. It's the first function with type Bool -> Bool -> Bool -> Bool that comes to mind, though.10/02 20:36
dolioSince I've read that thread.10/02 20:37
djahandarieAren't there a lot of functions with type Bool -> Bool -> Bool -> Bool? :P10/02 20:38
dolioYou have to be a little careful lifting definitional equations into reasoning equations, though.10/02 20:38
dolioBecause I can write down systems of equations that will behave in ways that are different than if you take particular lines as valid.10/02 20:39
copumpkindjahandarie: count them :)10/02 20:39
doliof 0 n = n ; f m 0 = 6 ; ...10/02 20:39
doliof 0 0 == 6? no.10/02 20:39
copumpkinyeah10/02 20:39
dolioAnd I suspect that recognizing which equations in a system are consistent is hard.10/02 20:42
dolioIn general, at least.10/02 20:42
--- Day changed Fri Feb 11 2011
djahandarieAny papers/talks/ideas connecting theorem proving and constraint solving / CSPs?11/02 01:32
djahandarie(I imagine they overlap a fair amount)11/02 01:32
copumpkindjahandarie: I have agda working!11/02 01:59
copumpkinyou have no excuse now11/02 02:00
djahandarie:(11/02 02:00
* djahandarie goes to get it working11/02 02:00
djahandariecopumpkin, okay.. I think it's working, but I'll need to actually try running something. :P11/02 02:18
copumpkinexcellent :)11/02 02:20
copumpkinyou should install the standard library too11/02 02:20
djahandarieThat needs to be done seperately? :P11/02 02:20
copumpkinyeah11/02 02:21
copumpkinyou on agda HEAD or the cabal version?11/02 02:21
djahandarieCabal.11/02 02:21
copumpkinhmm11/02 02:21
copumpkinnot sure which version goes with that11/02 02:21
copumpkinprobably 0.4 or something11/02 02:21
copumpkinhttp://www.cse.chalmers.se/~nad/software/lib-0.4.tar.gz11/02 02:21
copumpkinwell, you can get by just fine without the library, if you want11/02 02:22
djahandarieHmm11/02 02:22
djahandarieI'm not a fan of all the unicodeness11/02 02:22
copumpkinat least to play with things11/02 02:22
copumpkinfair enough11/02 02:22
copumpkinopen up emacs11/02 02:22
copumpkinwell, first type11/02 02:22
copumpkinagda-mode setup on your command-line11/02 02:22
copumpkins/-/ /11/02 02:23
djahandarieYeah I did that already11/02 02:23
copumpkinokay, yeah, so open up emacs and create a .agda file11/02 02:23
djahandarieYep11/02 02:23
copumpkinagda actually cares that the module name matches the filename11/02 02:23
djahandarieAh, so it'll have to be capitalized?11/02 02:23
copumpkinI think it'll allow a lowercase module name11/02 02:23
djahandarieGah11/02 02:23
copumpkinit doesn't ever care about case, afaik11/02 02:23
djahandarieI keep on typing .hs instead of .agda11/02 02:24
copumpkin:P11/02 02:24
djahandarieIt doesn't highlight?11/02 02:24
copumpkinit only highlights after loading the file11/02 02:24
copumpkinC-c C-l11/02 02:24
djahandarieAh11/02 02:25
gaschea beginner question11/02 09:36
gascheI'm stuck with one of the examples of Ulf Norell's Agda tutorial11/02 09:38
gaschehttp://pastebin.com/h41fvJjt11/02 09:38
gascheit's the lem-filter-All exercise, where you have to prove that all elements of the result of filter "satisfy" the predicate11/02 09:38
gaschemy problem is, I don't know how to have the typer understand that in the case where "p x" is true, "tt" is really of type (satisfies p x)11/02 09:39
gascheI hoped my second "with" clause would do that, but it actually doesn't solve the problem -- and therefore is useless11/02 09:40
gasche(the inferred type for the hole is (T (p x)))11/02 09:41
Saizanah, yeah, that happens because when the pattern matching rewrites p x to true the type of the goal is not in the context yet11/02 10:05
gascheso what should I do, introduce a spurious abstraction on (satisfies p x) as we sometimes do in Coq ?11/02 10:06
kosmikusdoesn't Ulf introduce "inspect"?11/02 10:06
Saizanyeah, inspect seems the idiomatic thing to use11/02 10:07
gascheok11/02 10:07
gascheit's a bit later in the tutorial, I will skip to that part then11/02 10:08
Saizanotherwise you could put "_:all:_ {P = p} {x} {xs}" in the with instead of T (p x) :)11/02 10:08
kosmikusSaizan: you mean "_:all:_ {P = satisfies p} {x} {filter p xs}" ?11/02 10:13
Saizanyes, sorry11/02 10:15
gaschethen11/02 10:17
gasche... | true | f = f tt (lem-filter-All p xs)11/02 10:17
gascheit works that way, thanks, but there is something I don't quite understand11/02 10:17
gaschehow do we pass {P = ...} as an implicit parameter, whereas it is declared as an explicit parameter of the All datatype ?11/02 10:17
kosmikusgasche: parameters that occur to the left of the colon in the datatype do automatically become implicit parameters of all the constructors11/02 10:18
kosmikusgasche: regardless of whether they're implicit or explicit for the datatype11/02 10:19
gascheok11/02 10:19
gaschewell I suppose I'm done, I'll read on Inspect and try to use it then11/02 10:20
gaschethanks for your help11/02 10:20
ppavelV6hi everybody11/02 20:41
Saizanhi11/02 20:41
copumpkinhi!!11/02 20:42
* ppavelV6 reading certified programming with dependent types11/02 20:43
copumpkinfunny, I just saw someone else tweet that they were reading that now11/02 20:44
copumpkinI guess more than one person might be reading the same book at the same time :)11/02 20:44
ppavelV6it wasn't mine, honestly :)11/02 20:44
ppavelV6copumpkin: no way. pauli exclusion principle would prohibit it!11/02 20:44
ppavelV6when i define something with Inductive Something .... in Coq it also defines Something_ind modulo sort for me. I'm not sure but this seems like a nice thing to have comparing to case splitting every time i use induction. Does agda have something similar ?11/02 20:47
copumpkinnope11/02 20:47
copumpkin:P11/02 20:47
ppavelV6I think so11/02 20:47
ppavelV6I would be surprised :) ]11/02 20:47
copumpkinif it does, I've never heard of it11/02 20:47
copumpkinwhich isn't really saying much11/02 20:47
ppavelV6And surprise is not your friend when programming :)11/02 20:47
copumpkinanyway, I've never seen an implicitly defined induction principle for any type11/02 20:48
copumpkinthey're pretty easy to write, if mechanical :P11/02 20:48
ppavelV6yep, but the add some noise11/02 20:48
copumpkinI think it's weird to have magical terms appear from a type definition11/02 20:49
ppavelV6copumpkin: agree11/02 20:49
copumpkinbut it is mechanical11/02 20:49
ppavelV6i'd prefer to have some magic to define them on need by need basis and probably a bit of reflection could help. or not :)11/02 20:49
copumpkinso I'm not sure what a good solution is. Possibly in a dependent language with reflection, a function called induction : forall A -> (x : A) -> InductionPrinciple A x11/02 20:50
ppavelV6Isn't Agda a dependent language with reflection? :)11/02 20:50
copumpkinnot that kind of reflection, sadly11/02 20:50
copumpkinI think epigram is getting it though11/02 20:50
copumpkin211/02 20:50
copumpkinas far as I know, agda's reflection is only for goal types11/02 20:51
ppavelV6hm... i can reflect on a type of current goal in agda, so probably ...11/02 20:51
ppavelV6yep11/02 20:51
ppavelV6have to think about it11/02 20:51
ppavelV6Does this mean that I can't mechanically build isomorphisms from records to Σ ?11/02 20:52
copumpkinI don't think so11/02 20:52
ppavelV6hmmm....11/02 20:52
copumpkinrecord structure is pretty opaque as far as I know11/02 20:52
ppavelV6it would be nice btw11/02 20:52
ppavelV6having records is a good thing but nested sigmas let us specify generic algorithms (like encoding record types, serialization etc)11/02 20:53
copumpkinI want extensible records :P11/02 20:53
copumpkinyeah11/02 20:53
ppavelV6copumpkin: ask Oleg :)11/02 20:54
copumpkinthe issue is how pleasant they are to use :P11/02 20:54
ppavelV6copumpkin:  yep :)11/02 20:54
copumpkinI can encode them to an extent in agda already, but the unification of fields in different orders is a nightmare11/02 20:54
ppavelV6I easily believe in this11/02 20:55
copumpkinprobably even more so when fields can depend on other field11/02 20:55
copumpkins11/02 20:55
ppavelV6what sigmas are about after all :)11/02 20:55
copumpkinyep :P11/02 20:55
copumpkinso yeah, built-in support for extensible records would make me 101% happy11/02 20:55
copumpkinthen I could go crazy on universal algebra and other structures11/02 20:55
* Saizan proposes a katagda11/02 20:57
ppavelV6I think I saw something in original thesis "Toward a practical ... "11/02 20:57
ppavelV6at least about record subtyping.11/02 20:57
ppavelV6Saizan: what it is supposed to be?11/02 20:57
SaizanppavelV6: kata is a, still not implemented, language ideated by an #haskell regular which is basically haskell minus types + a nice blend of extensible records/oo classes with very powerful inheritance11/02 20:59
ppavelV6Saizan: pardon me I lack the imagination powerful enough to immediately realize "haskell minus types"11/02 21:00
Saizanpurity, lazyness, pattern matching..11/02 21:02
ppavelV6dynamic typing?11/02 21:03
copumpkinand some degree of type-like stuff11/02 21:03
copumpkinwithout being explicitly typed11/02 21:03
copumpkinppavelV6: like no dynamic typing you've seen before :P11/02 21:03
copumpkinhis standard library is full of category theoretical structures that work nicely11/02 21:04
ppavelV6ok. i'm not sure all this oo stuff appeals to me very much since i traded Smalltalk for Haskell11/02 21:04
copumpkinin fact, his main design goal was for a language in which all that stuff nicely11/02 21:04
copumpkinit's not OO in any standard sense :P11/02 21:04
ppavelV6copumpkin: this sounds interesting :)11/02 21:04
copumpkinI'm trying to find his sample source file11/02 21:04
copumpkinhe's out of the office right now or I'd ask him11/02 21:04
copumpkinsince he normally sits next to me11/02 21:05
ppavelV6is it googlable?11/02 21:07
copumpkinnope11/02 21:08
ppavelV6so you just leaked something absolutely new :)11/02 21:08
Saizanheh, sorry if i've sidetracked the discussion :)11/02 21:08
ppavelV6:)11/02 21:08
copumpkinhttps://github.com/ekmett/kata is the closest you'll come to finding anything concrete about it, and there's #kata on freenode. But most of what I know about it has been edwardk talking about it in the channel or in person11/02 21:09
copumpkinhe wanted me to write his parser11/02 21:09
ppavelV6ok, probably i'm unprepared to dive into this now :)11/02 21:10
copumpkin:)11/02 21:10
ppavelV6reading Coq gets me headache :( It seem I will not be comfortable with syntax anytime soon11/02 21:12
dolioAgda takes pattern matching as primitive, so no auto induction principle (confirming from earlier).11/02 21:43
dolioThe primitive way to deconstruct inductive types is 'f (C <v>) = ...'.11/02 21:44
ppavelV6hmm.11/02 21:45
dolioWhereas Coq at least rewrites matching into eliminators in principle.11/02 21:45
pumpkindoes epigram2?11/02 21:45
pumpkin*will11/02 21:46
dolioI think so.11/02 21:46
dolioBut their universe of inductive types automatically comes with a generic elimination principle.11/02 21:46
pumpkinah11/02 21:46
pumpkindo inductive families get them free too?11/02 21:47
dolioelim : (D : Desc) -> ... -> Mu D -> R11/02 21:47
dolioYes. Although there it's IDesc, which generalizes Desc.11/02 21:47
dolioThere's also one for induction-recursion.11/02 21:48
pumpkinfancy!11/02 21:48
dolioActually, that elim isn't dependent enough, but you get the idea.11/02 21:50
dolioelim : (D : Desc) (P : Mu D -> Set) -> ... -> (x : Mu D) -> P x11/02 21:52
pumpkinyep11/02 21:52
dolioWith a fancy modal-looking operator in the ....11/02 21:52
dolioielim : (I : Set) (D : IDesc I) (P : forall i -> IMu D i -> Set) -> ... -> (i : I) -> (x : IMu D i) -> P i x11/02 21:55
pumpkinack11/02 21:56
--- Log closed Sat Feb 12 00:19:37 2011
--- Log opened Sat Feb 12 00:19:44 2011
-!- Irssi: #agda: Total of 33 nicks [0 ops, 0 halfops, 0 voices, 33 normal]12/02 00:19
-!- Irssi: Join to #agda was synced in 75 secs12/02 00:20
doliocopumpkin: Yes. We were supposed to talk today, but he rescheduled to Wednesday.12/02 00:31
copumpkindolio: ah, cool12/02 00:31
glguyDoes anyone know if it is possible (or reasonable) to provide an inductively defined relation for list permutation that has a unique implementation for each type?12/02 01:09
glguyhttp://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html is an example for Coq that does not have the unique property12/02 01:09
dolioI've tried, but it's usually difficult to prove all the properties of the relation you want.12/02 01:11
dolioThe one I used for proving my insertion sort correct includes transitivity as an axiom, so clearly it doesn't have unique representatives.12/02 01:12
dolioHey, it's actually the same one from that page, I think. :)12/02 01:13
jesnorhello anyone in?12/02 10:51
djahandariecopumpkin, so, how would I use something like Sigma in actual code?12/02 22:20
copumpkinhum12/02 22:20
copumpkinanywhere you'd use existentials in haskell, for one12/02 22:21
copumpkinanywhere you need to propagate values with proofs about them12/02 22:22
copumpkinplaces where you need to "forget" a type index of something12/02 22:22
copumpkinlike going from a Vec n a -> List a12/02 22:22
djahandarieI'm more at a loss of how to actually, well, do it.12/02 22:23
copumpkin?12/02 22:23
djahandarieI want some code that I can C-c C-l and observe :P12/02 22:24
copumpkinwrite x : \Sigma Bool (\lambda x -> if x then Bool else Nat)12/02 22:24
copumpkinx = true , false12/02 22:24
copumpkinoh you didn't install the standard library?12/02 22:24
copumpkinif not, then define sigma12/02 22:24
djahandarieNope. I have a definition already12/02 22:24
copumpkinand bool and nat :P12/02 22:24
copumpkinoh okay12/02 22:25
djahandarieNot of Bool and Nat though12/02 22:25
djahandarieDo I need to use \lambda for lambdas?12/02 22:25
copumpkinyou can just use \12/02 22:25
* djahandarie is not sure of how to define Bool or Nat. They don't feel like they would look like the Sigma definition12/02 22:26
copumpkindata Bool : Set where true : Bool; false ; Bool12/02 22:26
djahandarieAh, they would :P12/02 22:26
copumpkindata Nat : Set where zero : Nat; suc : Nat -> Nat12/02 22:26
djahandarieHmm, I don't have 'if' either12/02 22:27
djahandarieHow is that even a function with 'then' and 'else'?12/02 22:27
djahandarieAnd there is some flag or something to hook Nat into numerals, right?12/02 22:28
copumpkinif_then_else_ : forall a. Bool -> a -> a -> a12/02 22:28
copumpkinif true then t else f = t12/02 22:28
djahandarieOh, nice12/02 22:28
copumpkinif false then t else f = f12/02 22:28
copumpkin{-# BUILTIN NAT Nat #-}12/02 22:28
copumpkin{-# BUILTIN ZERO zero #-}12/02 22:29
copumpkinor something like that12/02 22:29
copumpkinthere's a suctoo12/02 22:29
djahandarieI think it's in the logs, I'll check12/02 22:29
djahandarie {-# BUILTIN NATURAL Nat #-}{-# BUILTIN ZERO zero #-} {-# BUILTIN SUC suc #-} -- apparently12/02 22:30
djahandarieIt doesn't seem to like the type of if_then_else_12/02 22:30
djahandarie/home/darius/agda/Test.agda:9,25: Parse error .<ERROR> Bool -> a ->12/02 22:30
copumpkinforall {a} Bool -> a -> a -> a12/02 22:31
djahandarieAh12/02 22:31
djahandarieRight12/02 22:31
copumpkinor {a : Set} -> Bool -> a -> a -> a12/02 22:31
Saizanforall {a} -> Bool -> ..12/02 22:31
djahandarieIt doesn't neccesarily need to be : Set though, right?12/02 22:31
copumpkinit could be at higher levels, but forall with that won't work12/02 22:32
copumpkinsince you need the level to be visible as well12/02 22:32
djahandarieHm, it still says 'if' isn't in scope. Does it need to be defined before the line I use it in or something?12/02 22:32
copumpkinforall {ell} {a : Set ell} -> Bool -> Bool -> Bool12/02 22:33
Saizan(<var> : <type>) works for any type, forall let you omit the : <type> part, but you'll get yellow (i.e. unsolved metas) if it can't be inferred12/02 22:33
copumpkinyeah, agda is sequential12/02 22:33
djahandarieWhoa, it typechecked12/02 22:33
djahandarieAnd false , 3 works, nice12/02 22:35
djahandarieSaizan, I don't understand12/02 22:36
dantenwhen you write forall {x} -> ... then Agda will infer what type x should have12/02 22:39
dantenor complain in yellow if it can't and you have to be explicit like {x : Set} -> ...12/02 22:40
djahandarieAh12/02 22:40
djahandariedata Vec (n : Nat) (B : Set) : Set where nil : Vec n B; cons : B -> Vec n B -> Vec (suc n) B  -- errors with  suc n != n of type Nat12/02 22:50
Saizansince n is before the : it can't vary between constructors12/02 22:51
djahandarieHm12/02 22:51
djahandarieSo that means it can't even be first12/02 22:52
Saizanyou've to say data Vec (B : Set) : Nat -> Set where ..12/02 22:52
djahandarieVec (B : Set) : Nat -> Set ..12/02 22:52
djahandarieYeah12/02 22:52
djahandarieWhy is that?12/02 22:52
Saizanby virtue of not being able to vary those before the colon, called parameters, don't count wrt the size of the type you're defining12/02 22:53
djahandarie... trying to load something just crashed emacs :P12/02 22:54
Saizanyou'd have to say Vec : Nat -> Set -> Set1 otherwise (or i guess we could require some smarter check for determining the size of the type)12/02 22:55
Saizansize = which universe it inhabits, here12/02 22:55
djahandarie"suc (_62 a) != n of type Nat" I don't understand what this error is telling me12/02 23:22
dantenit comes from unification, basically agda can't see why n should be a suc of something12/02 23:25
dantenit could be that you must be explicit about some implicit variable12/02 23:25
--- Day changed Sun Feb 13 2011
copumpkinam I not allowed to use irrelevant fields in types?13/02 01:27
copumpkineven if they're types of irrelevant things13/02 01:27
copumpkinI feel like I may have asked this before13/02 01:27
djahandarieHm, it feels like Agda *should* be able to type check this, but I keep on getting that error.13/02 01:29
copumpkin?13/02 01:30
copumpkinwhich error?13/02 01:30
djahandarieThe one I mentioned ~2hrs ago13/02 01:30
copumpkindanten told you what it was?13/02 01:31
djahandarieYeah, but I can't figure out how to fix it13/02 01:31
copumpkinneed moar code13/02 01:31
djahandariehttp://hpaste.org/43936/13/02 01:31
djahandarieCan't get units or pure to typecheck13/02 01:31
copumpkinyou can put the data type on different lines btw :)13/02 01:31
copumpkinI just used ; cause I was in IRC13/02 01:31
djahandarieYeah, I know, just haven't done it yet :P13/02 01:31
copumpkinfor pure13/02 01:32
copumpkinI'd switch the {A : Set} and {n : Nat} order13/02 01:32
copumpkinto make things cleaner13/02 01:32
copumpkinthen you need to make your recursive call to pure {n}13/02 01:32
copumpkinand pattern match on {suc n}13/02 01:32
doliocopumpkin: The Agda implementation doesn't do dependency on irrelevant things yet.13/02 01:32
copumpkindolio: :(13/02 01:32
copumpkinany hacks?13/02 01:33
djahandariecopumpkin, oh, I actually need to be explicit about that?13/02 01:33
dolioUse mini Agda. :)13/02 01:33
djahandarieHeh, well that was easy13/02 01:33
copumpkindjahandarie: it can't figure out that n is a successor and that it needs to be the predecessor in the recursive call13/02 01:33
copumpkindjahandarie: in general, it's a bad sign if you have a pattern match in one clause but not another13/02 01:34
copumpkin{zero} and {n}13/02 01:34
djahandarieAh, okay13/02 01:34
copumpkinthe extra knowledge that comes from knowing that {n} is actually {suc n} is usually helpful13/02 01:34
djahandarieGah I keep on accidently quitting emacs :P13/02 01:35
djahandarieImplicit params are weird :P13/02 01:36
djahandariecopumpkin, it feels like most of the functions I write should be able to generalize to any universe, but I'm not sure how to do that13/02 01:39
copumpkinenable universe polymorphism at the top of your file13/02 01:39
copumpkin{-# OPTIONS --universe-polymorphism #-}13/02 01:39
copumpkinthen you'll need to get some builtin levels13/02 01:40
copumpkinI can't remember how that works13/02 01:40
copumpkinI usually just import the standard one13/02 01:40
* djahandarie is reading wiki13/02 01:40
copumpkinmaybe it'll let you reuse your Nat type :)13/02 01:40
djahandariecopumpkin, BUILTINs LEVEL, LEVELZERO, ZEVELSUC, LEVELMAX, apparently13/02 01:51
djahandarieI suppose I could reuse my Nat type, but it's somewhat odd that it isn't done like that in the standard lib...13/02 01:51
djahandarieNATURAL and LEVEL have to be different types.13/02 01:53
djahandariewhen checking the pragma BUILTIN LEVEL Nat13/02 01:53
djahandarieSeems like it can't be done.13/02 01:53
copumpkinhah13/02 01:55
* copumpkin just proved identity arrows are unique in his toy CT library13/02 01:55
copumpkinvery exciting, I know13/02 01:55
dolioWhew. Finally proved that if A is HType n, A is also HType (suc n).13/02 03:26
copumpkinHType?13/02 03:27
dolioHomotopy type. From the univalent stuff.13/02 03:27
copumpkinoh13/02 03:27
dolioThe inductive step was easy, but the base case took a while.13/02 03:28
dolioI also proved that contractible types have unique identity proofs along the way.13/02 03:29
copumpkinI wish refining a large record would align the fields nicely13/02 03:46
copumpkinif I parametrize a category by its notion of equality, and construct a category out of a preorder13/02 04:11
copumpkinthe notion of equality of morphisms there is just true, right?13/02 04:11
dolioYes.13/02 04:15
copumpkinhmm, it seems like I can't make a pullback on any preorder13/02 04:27
copumpkinit has to be decidable13/02 04:27
copumpkinand the std lib doesn't have a decidable preorder13/02 04:28
copumpkinmaybe I should just go for the DecPoset13/02 04:31
copumpkinscrew the people who want to make preorder-but-not-poset categories13/02 04:32
copumpkin*pullbacks on them13/02 04:32
dolioWhy does it need to be decidable?13/02 04:33
copumpkinwell, I may be wrong13/02 04:33
copumpkinbut what is the "extra object" in the pullback?13/02 04:33
copumpkinnot sure what that's typically called13/02 04:34
copumpkinoh maybe I'm wrong13/02 04:35
dolioI'm not sure what you're attempting.13/02 04:35
dolioI doubt all preorders have pullbacks.13/02 04:35
copumpkinhmm, how about posets then13/02 04:36
dolioEven all decidable preorders.13/02 04:36
copumpkinyeah, the decidable thing was a red herring13/02 04:36
dolioConsider 0, 1, 2. f : 0 -> 2, g : 1 -> 2.13/02 04:37
dolioThat is a poset.13/02 04:37
dolioBut there is no pullback of f and g.13/02 04:37
dolioBy construction.13/02 04:37
copumpkinhmm13/02 04:37
copumpkinFrom TTT, "Identify pullbacks in a poset regarded as a category."13/02 04:37
copumpkindoes that suggest they're always possible? I interpreted it that way13/02 04:38
dolioThat sounds like, "assume a poset has pullbacks. What are they?"13/02 04:38
copumpkinoh, fair enough13/02 04:39
dolioglguy: By the way, about your question yesterday (I think)...13/02 05:24
glguypermutations?13/02 05:24
dolioRight. If you consider something like [2,2], it's hard to imagine that a type would only have one proof that it is a permutation of itself.13/02 05:25
dolioBecause there are two ways to pair up the elements.13/02 05:25
glguytrue13/02 05:26
glguyI was thinking about an abstract set without a decidable equivalence13/02 05:26
glguyat the time13/02 05:26
glguybut even then you can have13/02 05:26
glguy[x , x]13/02 05:26
dolioRight. You can still know that there are duplicate elements.13/02 05:27
copumpkinif I make a category that is parametrized by equality of objects13/02 05:57
copumpkinam I implicitly using agda's equality by talking about Hom B C -> Hom A B -> Hom A C?13/02 05:57
copumpkinit feels like I am13/02 05:57
copumpkinand should be talking about Hom A B -> Hom C D -> D ~ B -> Hom A C13/02 05:58
copumpkinor C A13/02 05:58
dolioObjects shouldn't have a notion of equality at all.13/02 05:59
glguymy experience with this is that as soon as you define the category of categories you die a horrible death13/02 05:59
copumpkindolio: that's what I thought13/02 05:59
copumpkinbut then ddarius asked me how I could define the arrow category for any category13/02 06:00
dolioYes, that's true.13/02 06:00
copumpkinglguy: *shudder*13/02 06:00
dolioYou can define a category by taking a set of objects and equipping it with arrows.13/02 06:00
dolioHowever, given a category, there isn't necessarily a set of objects of that category.13/02 06:00
glguyI did that with functors as my arrows... between agda eating all of my memory on records and the proofs about proofs I knew I'd gone down the wrong road13/02 06:01
copumpkinglguy: you mean parametrizing your categories by the equality relation?13/02 06:01
copumpkinequality on morphisms, that is13/02 06:01
copumpkinI was getting tired of postulating extensionality all over the place in ctfp13/02 06:01
copumpkinand convinced myself I only needed equality of morphisms13/02 06:02
copumpkindolio: so you're saying I shouldn't require object equality?13/02 06:03
dolioYes.13/02 06:03
copumpkinand should just ask for it when I try to build an arrow category?13/02 06:03
copumpkin(assuming I want to do such a thing)13/02 06:03
copumpkinoh wait13/02 06:04
copumpkinyeah13/02 06:04
dolioPresumably the arrows come with an equivalence relation or something.13/02 06:04
copumpkinyeah13/02 06:04
copumpkinit's actually good13/02 06:04
copumpkinI was just confusing myself13/02 06:04
dolioI wonder if code.haskell.org will be back any time soon.13/02 06:05
copumpkinI thought it was13/02 06:06
copumpkinbut they wanted individual repo owners to make sure their stuff wasn't infected13/02 06:06
dolioOh, hmm...13/02 06:06
dolioSo I actually have to do something to get my page back...13/02 06:06
copumpkinI think you might13/02 06:07
copumpkintalk to dcoutts13/02 06:07
copumpkindolio: was your CT thing parametrized on equality?13/02 06:11
dolioNope. I just postulated extensionality.13/02 06:12
copumpkinI see13/02 06:12
copumpkinugh, another agda bug13/02 06:12
copumpkinit seems to have shifted the holes by one13/02 06:13
copumpkinfairly easy to reduce though13/02 06:16
copumpkinhttp://code.google.com/p/agda/issues/detail?id=387 if anyone's curious13/02 06:20
dolioI must say, it's not obvious how the univalent axiom implies function extensionality.13/02 06:21
dolioHuh, that's an odd bug.13/02 06:22
copumpkinugh, I get creeped out when an odd computer shows up on my autodiscovered peers, when I'm on a WPA2-secured private network with a secure password and only have one other computer on the network :/13/02 06:22
copumpkin:P13/02 06:22
djahandarielol13/02 06:24
copumpkinI'm serious, it's creepy! :P13/02 06:24
copumpkinhorror stories for geeks13/02 06:25
glguyThis is why we need people using git and gpg signed tags (the code. hack)13/02 06:44
copumpkin?13/02 06:45
glguyany change to a git repository changes the names of the head commits13/02 06:45
glguyand git has built-in support for gpg signatures on tags13/02 06:46
copumpkinoh13/02 06:46
glguyso you don't have to wonder if an attacker altered your repository13/02 06:46
copumpkinI see, yeah13/02 06:46
copumpkindjahandarie: japanese tweets about agda, eh :)13/02 07:03
djahandarie:D13/02 07:03
djahandarieThere is at least one person who can understand it who I follow13/02 07:04
djahandarieBut he doesn't follow me :P13/02 07:04
djahandariehttp://twitter.com/#!/erutuf1313/02 07:04
djahandarieHe's actually younger than me lol13/02 07:04
copumpkinI've understood most of it so far :)13/02 07:06
djahandarieYou speak Japanese? :o13/02 07:06
copumpkinI took several terms of it in college and spent a summer there with a host family13/02 07:06
djahandarieOh wow, heh13/02 07:06
djahandarieThat's far more than I've done13/02 07:07
djahandarieI've actually done literally nothing :P13/02 07:07
copumpkina lot of it has faded, but I can still recognize many kanji and the phonetic alphabets13/02 07:07
djahandarieI'm making a lot of errors in these tweets, but oh well :P13/02 07:10
djahandarieI've managed to collect a few Japanese followers so they must be at least somewhat intelligible13/02 07:10
dolioJapanese type theorist followers?13/02 07:12
djahandariecopumpkin, you just made it into my next tweet :P13/02 07:16
djahandariedolio, so it seems...13/02 07:16
copumpkindjahandarie: I did? :o13/02 07:19
copumpkinoh I see13/02 07:20
djahandarie:P13/02 07:20
copumpkindolio: hmm, you still there?13/02 08:03
dolioYeah.13/02 08:03
copumpkinabout the decidable preorder pullback thing13/02 08:03
copumpkinI'm fairly convinced the pullback is just the glb13/02 08:03
copumpkinright?13/02 08:03
dolioYes.13/02 08:03
copumpkindon't I need decidable to actually talk about the glb?13/02 08:04
copumpkinin the sense of being able to figure out which of the two is larger, return it13/02 08:05
copumpkinreturn the other one, I mean13/02 08:05
dolioA glb isn't necessarily one or the other.13/02 08:05
dolio0,1,2,3, f : 0 -> 1, g : 0 -> 2, h : 1 -> 3, k : 2 -> 313/02 08:06
doliothe pullback of h, k is (0,f,g).13/02 08:06
copumpkinoh, yeah, I was thinking too narrowly13/02 08:07
copumpkinbut how would I define glb then, for this purpose?13/02 08:07
copumpkina meet semilattice?13/02 08:07
dolioAnyhow, I guess it's more like glb, but only required to exist for two objects with a common upper bound.13/02 08:08
dolioI'm not sure what you call that.13/02 08:08
dolioProducts are glbs in general.13/02 08:08
copumpkinso I basically need some structure preorder + glb, to make a pullback13/02 08:08
copumpkinyeah13/02 08:08
copumpkinbut I don't necessarily have products yet here13/02 08:09
copumpkinI guess I can just ask for a category with products :)13/02 08:10
copumpkinbinary ones, anyway13/02 08:10
dolioSo, for instance, if you had 2 (disjoint?) sets S and T, you could make a partial order where objects are subsets of one or the other, and arrows are the subset relation.13/02 08:11
dolioActually, that's a bad example, because the empty set is common to both.13/02 08:12
dolioOkay, instead, make such a category with S and with T and take their coproduct.13/02 08:15
dolioThen, you don't have products, because if you take an S subset and a T subset, there's no glb for them.13/02 08:15
dolioHowever, it has pullbacks, because the diagram ensures that you're dealing either with two subsets of S or two subsets of T.13/02 08:16
copumpkinbecause of the third object they're both less than?13/02 08:17
dolioRight.13/02 08:17
copumpkinhm, yeah13/02 08:17
copumpkinso I guess there's not a succinct way to describe the requirement for there to be a pullback on a preorder other than just describing the conditions (basically the pullback constructs, minus all the laws that are satisfied automatically by it being a preorder)13/02 08:18
dolioI'm not sure there are any conditions satisfied by it being a preorder.13/02 08:20
dolioOther than uniqueness of morphisms.13/02 08:20
copumpkinwell, I mean most of the laws about squares commuting and the universality stuff is trivial because arrows are unique and equal13/02 08:20
copumpkinyeah13/02 08:21
dolioAnyhow, on a semi-related note, the Set category in Agda has pullbacks, but I wouldn't call its objects decidable.13/02 08:22
dolioCertainly given X, Y : Set X == Y is not decidable.13/02 08:22
copumpkinyeah, but that's different13/02 08:22
copumpkinthe preorder set category in agda would be ordered by subset-ness13/02 08:23
copumpkinwouldn't it?13/02 08:23
copumpkinthe usual one is just a "join" of sorts13/02 08:23
copumpkinI have a pullback for the common agda category in ctfp, anyway13/02 08:24
copumpkinthat performs something a bit like a relational join13/02 08:24
dolioYou can probably define a subset preorder for any type in Agda, I guess.13/02 08:25
copumpkinusing Sigma?13/02 08:25
dolioA -> Set being the type of the objects.13/02 08:26
copumpkinI see13/02 08:26
dolioAnd for X, Y : A -> Set, X < Y = forall a -> X a -> Y a?13/02 08:26
dolioEr, <=.13/02 08:27
copumpkinyeah13/02 08:27
copumpkinI guess actual members of these would be sigma values13/02 08:27
copumpkinI think NAD has something like what you're describing in one of the Relation.* modules13/02 08:28
dolioThen, for X, Y, Z, X <= Z and Y <= Z, the pullback is \a -> X a * Y a13/02 08:28
dolioWhich is the same as the product.13/02 08:28
copumpkinyeah13/02 08:29
copumpkinhttp://web.student.chalmers.se/~stevan/ctfp/html/Relation.Unary.html#461213/02 08:29
dolioI should note, my example with the two sets....13/02 08:42
dolioThe category has products. Whenever X and Y have a pullback, that pullback is also a product.13/02 08:42
dolioIt just doesn't have all products.13/02 08:42
dolioBecause there are choices of X and Y without products.13/02 08:42
dolioHowever, it has all pullbacks, because the definition of a pullback rules out the offenders.13/02 08:43
copumpkinyheah13/02 08:43
copumpkinmakes sense13/02 08:43
copumpkinalright, bedtime13/02 08:46
dolioNight.13/02 08:46
copumpkinnight13/02 08:46
copumpkinthese shifted goals are fucking with my head13/02 17:16
Saizannever found ones that kept being shifted after a reload13/02 17:22
copumpkinmine are always shifted :(13/02 17:26
copumpkindid you see the bug I filed?13/02 17:27
Saizanyep13/02 17:27
copumpkinmaybe I should just fill in that type hole13/02 17:52
copumpkin  PullbackBuilder a b c = (f : Hom a c) (g : Hom b c) → Pullback f g13/02 18:35
copumpkinthat seems unnecessary13/02 18:35
copumpkinbut every pullback I build is going to look like that13/02 18:35
copumpkinanyone have a better idea?13/02 18:35
copumpkin(I parametrize by the objects so I can refer to them in other "prerequisites")13/02 18:36
djahandarieWould it be possible to define List in terms of a Vec that just forgets about its length?13/02 19:01
copumpkinsure13/02 19:01
copumpkinwrap a sigma around it :)13/02 19:01
copumpkinbasically List a = exists n. Vec n a13/02 19:01
copumpkin'tis the beauty of sigma13/02 19:02
copumpkinbut unlike haskell, you can pattern match on that n later if you want to13/02 19:02
copumpkin(not that you need to in this case)13/02 19:02
copumpkinsigma is all about forgetting specifics!13/02 19:02
djahandarieI understand the idea... but doesn't Sigma mean you're going to need to have that length proof on the value level?13/02 19:03
copumpkinhow do you mean? it'll carry around the length unnecessarily, yeah13/02 19:04
* djahandarie doesn't fully understand, he thinks13/02 19:04
copumpkinfor true forgetfulness, you'll want conor's recent stuff on algebraic ornaments, ornamental algebras13/02 19:04
sullyhow is sigma defined, again?13/02 19:05
copumpkindata Sigma (A : Set) (B : A -> Set) : Set where _,_ : (x : A) -> B x -> Sigma A B13/02 19:06
copumpkinplus universe polymorphism, plus record13/02 19:06
copumpkinbut both its parameters are relevant13/02 19:06
sullywhy do you need universe polymorphism and record there?13/02 19:06
copumpkinI've often needed a version with an irrelevant second half, and djahandarie needs an irrelevant first half13/02 19:06
copumpkin(I think)(13/02 19:06
copumpkinsully: records lets you prove that all constructors are _,_ without pattern matching on it13/02 19:07
copumpkinand universe polymorphism just gives you more flexibility13/02 19:07
copumpkinyou can stick in things at any level instead of just Set13/02 19:07
copumpkinany of you have an excellent font for agda editing? I just want a monospace font that contains lots of symbols, and actually monospaces them (so things line up nicely even when there are crazy symbols)13/02 19:20
sullyEmacs.font:  -misc-fixed-*-10-*13/02 19:21
sullyis what I apparently use?13/02 19:21
sullyI would not claim that it is "excellent"13/02 19:21
sullyor exactly what it is13/02 19:22
copumpkinI generally like consolas, but the spacing is irregular when I get lots of unicode13/02 19:22
glguyThe monospaced fonts start to get hard when you use \--> and other symbols that don't fit well into the space allotted13/02 19:26
copumpkinyeah :/13/02 19:26
* copumpkin changes his editing font to zapfino13/02 19:26
djahandariecopumpkin, dejavu sans mono?13/02 19:35
glguyI use Monaco13/02 19:35
djahandariecopumpkin, could you give me an example of using Sigma to forget the length?13/02 19:37
glguySigma Nat (\ n -> Vec A n)13/02 19:38
copumpkinyou can also use Exists there13/02 19:38
copumpkin\exists (Vec a)13/02 19:38
djahandarieYeah, that's what I thought, and it isn't really what I want13/02 19:38
copumpkinhmm, how so?13/02 19:38
djahandarieBecause then you need to deal with providing the length on the value level, right? I just want to forget about it entirely13/02 19:39
djahandarieI might not be using the word 'forget' formally here13/02 19:40
copumpkinyou can write a function (even make it n-ary) to magically transform functions (Vec n a -> Vec m b) -> (List a -> List b)13/02 19:40
glguycopumpkin: I don't think you can have an irrelevant first argument used to index a relevant second13/02 19:42
copumpkinyeah, you're right13/02 19:42
Saizanyou can't index arguments by irrelevant ones at all, though i guess if the other is irrelevant too you could just take a single irrelevant record13/02 19:43
copumpkinthe sigma with irrelevant snd is still useful for me though13/02 19:43
copumpkinI actually needed it for slice categories in ctfp13/02 19:44
djahandarieCTFP?13/02 19:51
djahandarieCategory theory functional programming? :P13/02 19:51
copumpkinhttp://web.student.chalmers.se/~stevan/ctfp/html/README.html13/02 19:51
djahandarieNeat13/02 19:52
copumpkinhttp://web.student.chalmers.se/~stevan/ctfp/html/Category.Categories.Comma.html#30913/02 19:53
copumpkinthat's where I needed the half-irrelevant sigma13/02 19:53
djahandarieThe unicode... it burns my eyes ;_;13/02 19:53
copumpkin:P13/02 19:53
copumpkinyeah :)13/02 19:54
copumpkinit's not that bad though13/02 19:54
djahandarieYou can define coslice in terms of a comma category too right?13/02 19:55
copumpkinyeah13/02 19:57
copumpkinand arrow13/02 19:57
copumpkinI haven't gotten around to doing any of that13/02 19:57
copumpkinwill probably do it in my own library13/02 19:57
copumpkinsince I dislike being tied to agda's propositional equality13/02 19:57
copumpkinand am too lazy to go fixing all the definitions in that library to use a category's own equality13/02 19:58
djahandarieWhere is your library? :)13/02 19:58
copumpkinplus, I'd like to take it in a different direction13/02 19:58
copumpkinon my computer13/02 19:58
djahandariegit it :P13/02 19:58
copumpkinjust made a github repo but haven't put it up yet13/02 19:58
copumpkinyeah13/02 19:58
copumpkinI really wish the standard library hadn't eaten the Category module namespace13/02 19:59
djahandarieWho needs the standard library anyways :P13/02 19:59
* pumpkin should probably pack13/02 20:11
copumpkinon train!13/02 22:48
djahandarieWhere are you heading copumpkin?13/02 22:50
copumpkinNYC13/02 22:50
djahandarieCool, what for?13/02 22:50
copumpkinjust work13/02 22:51
copumpkindown there until saturday13/02 22:51
djahandarieI wish my job would send me places :P13/02 22:51
dolioI interviewed at a place not long ago: 30% - 50% travel. Maybe you should look for a similar place.:)13/02 22:52
copumpkintravel is overrated :P13/02 22:53
copumpkinNYC isn't13/02 22:53
copumpkinwork travel, anyway13/02 22:53
dolioYeah, NYC is cool.13/02 22:53
copumpkinmy dad used to travel most of the time for his job, said it was fun at first but got old pretty quickly13/02 22:53
glguyIs there a good name for this? ∀ {x y} → ¬ (x ≤ y) → y ≤ x13/02 23:01
copumpkinantisymmetry?13/02 23:01
copumpkinnot quite, I guess13/02 23:01
copumpkinasymmetric: for all x and y in X it holds that if xRy then not yRx. "Greater than" is an asymmetric relation, because if x>y then not y>x.13/02 23:02
copumpkinhttp://en.wikipedia.org/wiki/Asymmetric_relation13/02 23:03
glguyI avoided needing that operation by using "total" directly13/02 23:03
dolioThat isn't what the type says, though, unless you're using DNE.13/02 23:03
copumpkinyeah13/02 23:04
glguyI get this pattern a lot (in a local case):  P x -> P y -> P (f x y)13/02 23:16
glguyIs this something that has a name people would recognize13/02 23:16
glguyI can make up names, but I don't want to hide meaning13/02 23:16
copumpkinit's sort of like a liftA2 in the type index :)13/02 23:17
copumpkinother than that, not sure what I'd call it13/02 23:18
dolioIt's the inductive step in f-induction.13/02 23:18
copumpkinman, I'm even having trouble writing an opposite category in this thing13/02 23:29
copumpkinin a slice category, equality on morphisms is simply equality on the underlying morphisms, right? it seems silly to ask the commutative proofs to be equal13/02 23:55
copumpkinwhat might I need a proof that == respects morphism composition for?13/02 23:59
copumpkintrying to figure out if my statement is strong enough13/02 23:59
--- Day changed Mon Feb 14 2011
copumpkindo I get subst on an arbitrary equivalency relation?14/02 00:07
copumpkinhmm, it seems not :(14/02 00:14
copumpkinlol14/02 00:22
copumpkinI can't C-c C-d to ask for the type of an irrelevant field in a non-irrelevant context14/02 00:22
* glguy doesn't quite understand why this definition of merge passes the termination checker http://www.galois.com/~emertens/merge/mergeexample.html#227214/02 00:28
glguyit seems to hinge on the recursive case being in a with clause14/02 00:28
copumpkinthat does seem tricky14/02 00:33
copumpkinbut recursive calls are getting smaller14/02 00:33
glguyAgda only seems to see the lexicographic order in the with clause14/02 00:34
glguyotherwise it just draws red boxes all over my code!14/02 00:34
copumpkinodd14/02 00:34
copumpkindoes your Permutation inductive type cover all permutations?14/02 00:36
glguyI believe it does14/02 00:36
copumpkinI once tried constructing something similar and thought there were ones that it didn't cover14/02 00:36
copumpkinhmm, maybe you're right14/02 00:36
copumpkinit's odd to get a parse error when I ask agda to refine something14/02 01:05
copumpkinokay, I guess I needed it to build slice categories14/02 01:29
dolioglguy: Does it complain when you inline the merge calls?14/02 02:10
glguyyes14/02 02:14
dolioWell, I think the explanation is this:14/02 02:19
dolioWhen you use them in the with, the recursive calls are happening within the original function, so they are clearly decreasing.14/02 02:19
doliowiths desugar into an auxiliary function with additional arguments.14/02 02:19
dolioWhen you inline them, the recursive calls are happening in the auxiliary.14/02 02:20
dolioAnd I don't know how variables from a pattern are passed to the auxiliary, but it may well look like 'aux x xs y ys ... = ... merge (x :: xs) ys ...'14/02 02:21
dolioWhich looks like it's growing.14/02 02:21
dolioPotentially you could increase the termination checker depth to make it smarter in this case.14/02 02:22
dolioHaving the recursive calls in the with is equivalent to something like 'merge (x :: xs) (y :: ys) = aux x xs y ys (total x y) (merge xs (y :: ys)) (merge (x :: xs) ys)'.14/02 02:23
dolioI suspect if you manually desugar that way, you'll see the same thing.14/02 02:27
nh2hey people! Can somebody help me with some first steps in agda? I just apt-got agda-bin and want to compile some basic example from a plain file without emacs, but the whole internet seems to lack a tutorial for that :(14/02 02:28
dolioI don't think I've ever compiled Agda.14/02 02:29
dolioIn other words, I recommend playing in emacs. :)14/02 02:31
nh2dolio: can Agda actually do some input/output like in Haskell? I currently want to see if I can write a small program that reverses input, using functions I would like to prove correct14/02 02:35
dolioYes. It has the ability to import functions from Haskell, and some IO stuff has been imported into the standard library.14/02 02:36
dolioI'm not sure I've ever used it, though.14/02 02:37
nh2dolio: after a lot more googling, it is running fine with agda -i14/02 03:20
nh2I wonder however about the following thing:14/02 03:20
nh2I have defined some Nats, - function that returns 42 if n>x in x-n and a fib function where fib zero = suc zero, fib (suc zero) = suc zero and fib n = fib (n - (suc zero)) + fib (n - (suc (suc zero)))14/02 03:22
nh2why does not that pass the termination check?14/02 03:22
nh2I mean: doesn't Agda know that if zero and suc zero don't match, that the argument must then at least be suc (suc zero) ?14/02 03:23
dolioThe termination checker can't tell than n - (suc zero) is smaller than n.14/02 03:23
dolioNo, it isn't that fancy.14/02 03:24
nh2dolio: is it because it is not implemented yet or because that is definitely not possible by theory?14/02 03:24
dolioI won't say that it isn't possible, but it's asking a lot more intelligence than it has.14/02 03:25
dolioI don't think it uses any information from the previous cases in the last case.14/02 03:26
dolioSo it doesn't keep track of the fact that n = suc (suc m) for some m.14/02 03:26
nh2dolio: perfect! I think this whole stuff is a damn interesting research area14/02 03:27
dolioKnowing that n = suc (suc m) would probably be more the coverage checker's area, which is probably separate.14/02 03:28
nh2I found a good example on how to compile with agda: the readme of https://github.com/agda/agda-system-io/14/02 03:44
kfishimplicit Style14/02 04:18
* glguy loses his mind juggling this proof over an arbitrary setoid14/02 05:29
glguydoing thing manually because you don't learn that things are equal when you pattern match is craziness14/02 05:29
copumpkinwow, that's exactly the problem I've been having with my new categories :)14/02 05:31
copumpkinI basically have a setoid of arrows14/02 05:31
glguy     = antisym (proj₁ ≤-resp-≈ b y) (proj₁ ≤-resp-≈ (≈-sym a) y1)14/02 05:31
glguylines and lines of stuff like this :)14/02 05:31
dolioSetoids are a pain.14/02 05:31
copumpkinand all my clean, elegant rewrites and pattern-matches on refl are lost14/02 05:31
copumpkinreplaced by ugly equational reasoning about things that should be obvious14/02 05:31
copumpkintrans (trans (sym (∘-assoc a⇒b b⇒c c⇒x)) (∘-resp-≡ (c⇒x ∘ b⇒c) b⇒x a⇒b a⇒b pf₁ (IsEquivalence.refl ≡-equiv))) pf₂14/02 05:32
copumpkinthat's one of mine14/02 05:32
copumpkinbonus points if you can figure out what it is based on that :)14/02 05:33
glguyat least with a pile of trans you can use PreorderReasoning14/02 05:33
copumpkinyeah, I could I guess14/02 05:34
copumpkincan't you? your setoid has an equivalence relation with trans14/02 05:34
copumpkinI guess not for these particular proofs?14/02 05:34
glguyI don't have many trans uses14/02 05:35
copumpkinI've found myself wanting subst a lot :(14/02 05:35
copumpkincan it be written for an arbitrary equivalence relation?14/02 05:35
copumpkinprobably not, e14/02 05:36
copumpkinh14/02 05:36
glguyEqReasoning for an artibrary setoid, PreorderReading for a ...14/02 05:36
kfishcopumpkin, nice slides!14/02 06:35
djahandarieSlides? Where? :o14/02 06:38
djahandarieAh drats, I forgot to remind edwardk to upload the boston haskell videos for like the 3rd weekend in a row14/02 06:39
kfishhttp://dl.dropbox.com/u/361503/Agda%20and%20dependent%20types.pdf14/02 06:51
kfish(from #haskell a little while ago)14/02 06:51
djahandarieAh nice, thanks14/02 06:53
djahandarieFeels awfully like what I've been learning recently :P14/02 06:56
djahandarieAh nice, this proofs section at the end is useful14/02 07:02
* djahandarie thanks copumpkin even though he's sleeping14/02 07:02
glguyI'll grant that I'm not picking "good names" here, but14/02 07:59
glguy  hardpart eq (y3 ∷ y4 ∷ y5) (cons y0 y2) (swp y6 y7 y8) = tran (≈-trans (≈-trans y4 y7) (≈-sym eq) ∷ ≋-trans y5 y8) y2 (cons (≈-trans (≈-trans y0 y3) y6) perm-refl)14/02 07:59
glguyand for reference:   hardpart : ∀ {x y b c d e} → x ≈ y → c ≋ d → Permutation (x ∷ b) c → Permutation d (y ∷ e) → Permutation b e14/02 08:00
* glguy is just doing what C-c C-, tells him to at this point...14/02 08:02
* glguy is stuck at perm-uncons : ∀ {w x z} → Permutation (w ∷ x) (w ∷ z) → Permutation x z14/02 09:51
glguytransitivity as an axiom is a bear :)14/02 09:51
* Saizan wonders if bear is positive or negative there14/02 12:42
dolioSaizan: Negative, I expect.14/02 20:43
jlouisagda2 is such a memory hog14/02 22:18
corpumpkinjlouis: indeedles!14/02 22:19
jlouiswhy?14/02 22:20
jlouisthe infinite laziness crap strikes again?14/02 22:20
corpumpkincause the terms are very large!14/02 22:20
corpumpkinuse moar irrelevance14/02 22:21
corpumpkinit helps a bit14/02 22:21
jlouisI see14/02 22:21
djahandarieOh by the way corpumpkin, I managed to propegate your slides to a bunch of Japanese Agdaers :P14/02 22:22
corpumpkindjahandarie: I noticed ikegami tweeting at me :)14/02 22:22
copumpkingotta go14/02 22:25
--- Day changed Tue Feb 15 2011
* copumpkin wonders if the isEquivalence in Setoid could be made irrelevant15/02 01:38
copumpkincan I have an irrelevant module?15/02 01:42
copumpkin(one that can be opened only in irrelevant contexts)15/02 01:43
dolioI don't think so.15/02 01:43
copumpkincan you think of anything wrong with the idea in principle?15/02 01:44
dolioI have no idea how modules embed into the type theory, if at all.15/02 01:45
dolioYou can have an irrelevant record, of course.15/02 01:45
copumpkinyeah15/02 01:47
copumpkinworking with generalized equality is getting easier as I get used to it15/02 02:00
dolioA language that made working with setoids more like working with equality would be nice, though.15/02 02:06
dolioCoq has some kind of setoid rewrite, but I'm not sure what all that gets you.15/02 02:06
dolioOf course, with quotients you can just make an equivalence relation into equality by fiat.15/02 02:09
dolioHowever, it may be desirable to work with respect to the equivalence relation only in a limited portion of the program, where the quotient would screw you when you tried to get back out of it.15/02 02:10
copumpkinhmm, this is starting to take a couple of minutes to typecheck each time15/02 02:14
copumpkinmaybe it's a sign that it's time to break it into modules15/02 02:14
copumpkinwell, there, opposite, slice, arrow categories on categories parametrized by equality, and for fun, pullbacks too15/02 02:25
copumpkinweird15/02 02:57
copumpkinanyone have any clue why importing a module that typechecks fine would give me an error15/02 02:57
copumpkinhttp://snapplr.com/479915/02 02:57
copumpkinseems odd15/02 02:58
copumpkinoh, hmm15/02 03:01
dolioWow.15/02 03:01
copumpkinit's actually the original module I'm importing giving me that error15/02 03:02
copumpkinhave no clue how though15/02 03:02
copumpkinhttp://snapplr.com/ew3515/02 03:02
copumpkinnot a very informative message15/02 03:02
copumpkinweird15/02 03:24
copumpkinit was a universe level issue15/02 03:24
copumpkinI mean15/02 03:25
copumpkinduh15/02 03:25
copumpkinbut one where a record didn't fit into the universe I'd given it15/02 03:25
copumpkinis there some way to make this cleaner? http://snapplr.com/eckc15/02 04:29
copumpkinit feels a bit like a lisp right there :)15/02 04:37
copumpkinbut it was the nicest nesting I could think of15/02 04:37
dolioUse eq reasoning.15/02 05:04
* glguy_ would love help thinking of a way to encode permutations which supported an "uncons" operation... x = y -> Permutation (x :: xs) (y :: ys) -> Permutation xs ys15/02 05:25
glguy_(I guess I could always add that in as a constructor...15/02 05:25
dolioglguy_: Presumably you should be able to prove that.15/02 06:13
dolioBy induction on the proof structure.15/02 06:14
dolioAlthough, depending on what your proof looks like, it could be bad.15/02 06:14
djahandariecorpumpkin, is your site down?15/02 21:59
corpumpkinoh yeah15/02 22:00
corpumpkinI think that same code is up on hpaste somewhere15/02 22:00
djahandarieI only see the Haskell one you wrote15/02 22:01
corpumpkinI'll put it back up later15/02 22:03
djahandarieOkay15/02 22:03
* djahandarie drives home in that case15/02 22:04
--- Day changed Wed Feb 16 2011
djahandariecorpumpkin, hurry up and drop that code somewhere, I'm getting to the point where I'm going to need some include some code ;)16/02 01:38
djahandarieHmm, it's easy to get really wordy when talking about this stuff. :P16/02 02:43
copumpkinyou have a blog?16/02 02:47
djahandarieI don't16/02 02:49
copumpkinwhere you gonna put your writing?16/02 02:50
djahandarieMy site probably16/02 02:50
djahandarieJust as a static page16/02 02:50
copumpkinah ok16/02 02:50
copumpkinthat reminds me, I was going to put the site back up16/02 02:50
djahandarieYes, do it :)16/02 02:50
copumpkinhttp://pumpkinpat.ch/moo.html16/02 02:51
djahandarieYeay16/02 02:51
djahandarieHow do I get that code highlighting16/02 02:51
copumpkin:P16/02 02:51
djahandarie>:)16/02 02:51
copumpkinthere's a horrific highlighter I threw together a while back16/02 02:51
copumpkinI think it's on my github16/02 02:52
djahandarieDoesn't hpaste have one?16/02 02:52
copumpkinbut you'll need to hack at it16/02 02:52
copumpkinnope16/02 02:52
djahandarieBah16/02 02:52
djahandarieMight just highlight it manually :P16/02 02:52
copumpkinwell, agda can generate nicely highlighted docs16/02 02:52
copumpkinbut you get craploads o' links16/02 02:52
djahandarieIt doesn't just have a flag to like, turn that off?16/02 02:53
copumpkinnot that I know of16/02 03:10
* copumpkin can't think of an elegant way to express products16/02 03:10
copumpkinthe problem with http://web.student.chalmers.se/~stevan/ctfp/html/Category.Product.html#396 is that it's basically "all binary products" rather than "a product"16/02 03:11
copumpkinbut I'd still like to be able to talk about A x B16/02 03:12
copumpkinas being an object16/02 03:12
doliohttp://hpaste.org/44026/products16/02 03:20
dolioThat's how I did it.16/02 03:21
copumpkinoh, fair enough16/02 03:21
copumpkinI considered something like that16/02 03:21
copumpkinbut was reluctant to hardcode the name in there16/02 03:21
copumpkinoh I see16/02 03:22
copumpkinyou get _x_ for having binary products16/02 03:22
dolio_Product packages up an object and the stuff that makes it a product for A and B.16/02 03:23
dolio_Has-Products states that there is a _Product for each A and B.16/02 03:23
copumpkinyeah16/02 03:24
copumpkinI might use your approach, if you don't mind16/02 03:31
doliocopumpkin: Go ahead.16/02 03:39
copumpkin   where open Reasoning (A×B ⇒ A×B)16/02 03:39
copumpkindoes that mean you have a setoid?16/02 03:39
dolioNo. I was using eq reasoning for propositional equality.16/02 03:39
copumpkinah okay16/02 03:40
copumpkinalso16/02 03:43
77CAAQQ6Idolio: I don't think that my "uncons" lemma for permutations (using the common transitive closure of swaps) is a simple matter of induction..16/02 03:43
copumpkindolio: any particular reason you went with <_,_> over the more conventional definition?16/02 03:44
77CAAQQ6Ibut I might not be starting from a general enough type16/02 03:44
copumpkin77CAAQQ6I: are you glguy? :P16/02 03:44
copumpkinI guess so16/02 03:44
77CAAQQ6Ioh, weird16/02 03:44
copumpkindid you see NAD's suggestion?16/02 03:44
glguy_no16/02 03:45
glguy_I'll scroll and check16/02 03:45
doliocopumpkin: Conventional?16/02 03:45
dolioI used the one from category theory.16/02 03:45
dolioglguy_: Probably not simple, no.16/02 03:45
copumpkindolio: hmm, okay :)16/02 03:46
copumpkinglguy_: I mean his email16/02 03:46
copumpkinhe sent the three of us an email :O16/02 03:46
glguy_hmm.. could you forward that to me?16/02 03:48
copumpkinare you not emertens@gmail.com ?16/02 03:49
copumpkinthat was the primary recipient, and dolio and I were CC'd16/02 03:50
dolioWhen was this?16/02 03:50
copumpkinearlier today16/02 03:50
glguy_That's me, but I didn't get it16/02 03:50
copumpkinwow, weird16/02 03:50
copumpkinhttp://snapplr.com/heyn16/02 03:50
dolioWell, I didn't get it either. Maybe gmail spam filtered it.16/02 03:50
glguy_It wasn't in my gmail spam folder either16/02 03:50
dolioAh yes. Found it.16/02 03:51
* glguy_ clicks on the image futilely16/02 03:51
djahandariecopumpkin, notice the tag gmail give it16/02 03:52
djahandariegave*16/02 03:52
copumpkinglguy_: let me forward it to you16/02 03:52
djahandarieYou have probably sent emails back and forth to dolio/glguy/nad so gmail let it through just because of that16/02 03:52
glguy_I typed the links out16/02 03:52
copumpkinaw16/02 03:52
copumpkinyeah, I've conversed with NAD before16/02 03:53
dolioI should have mentioned the BagAndSetEquality. I haven't looked at it enough to understand it, but he seems to have a definition of permutation that works well there.16/02 03:53
glguy_I wonder if this deals with lists with multiple occurrences of elements16/02 03:55
glguy_today I actually tried using a type exactly like Data.List.Any's Any type16/02 04:03
glguy_and a list that build up a permutation using them16/02 04:04
dolioI've tried that too.16/02 04:06
dolioDoesn't work out so well.16/02 04:06
glguy_yeah, it was roughly a disaster :)16/02 04:06
dolioEverything I've tried makes it hard to write either sym or trans.16/02 04:08
dolioOr both.16/02 04:08
dolioExcept that one definition with nil, cons, swap and trans.16/02 04:09
copumpkindolio: odd that I have to use your commute\_1 and commute\_2 in g-\eta, where you can use refl16/02 04:29
copumpkinI guess not that odd16/02 04:29
dolioI think those are pi_n . i == pi_n . i16/02 04:32
copumpkinmy \eta is way simpler though16/02 04:32
copumpkin  .η : ⟨ π₁ , π₂ ⟩ ≡ id16/02 04:33
copumpkin  η = universal π₁ π₂ id (commute₁ π₁ π₂) (commute₂ π₁ π₂)16/02 04:33
bxc_anyone know about linear types in agda? i saw oleg has some stuff about linear types in haskell using parameterised monads, but is thre anything agda specific?16/02 11:23
pigworkerbxc_: if you want to model a linearly typed DSL, there's a thing you can do...16/02 11:50
pigworkerdefine a two element type {alive,dead}, take contexts to be lists of pairs of types and alive-or-deads16/02 11:52
pigworkerdefine variables indexed by type and contexts before *and after*, explaining what it is to kill a variable of a given type16/02 11:53
pigworkerVar : Cx -> Ty -> Cx -> Set16/02 11:54
pigworkertop : forall {g t} -> Var (g :: (t , alive)) t (g :: (t , dead))16/02 11:54
pigworkerpop : forall {g g' x t} -> Var g t g' -> Var (g :: x) t (g' :: x)16/02 11:55
pigworkerDefine terms similarly, with before-and-after contexts. You thus ensure that vars are used at most once, and if you insist that they all end up dead, exactly once.16/02 11:56
pigworkerIndeed, the context-threading makes terms a parametrised monad16/02 11:57
bxc_ok cool16/02 12:14
bxc_when my brain wakes up a bit more I'll play some more - thanks16/02 12:18
starcloudedhello everybody16/02 17:01
starcloudedanyone could explain to me in a few words the Curry-Howard isomorphism?16/02 17:02
freiksenetprograms are proofs16/02 17:03
freiksenetthat kinda sums that16/02 17:03
freiksenet(and vice versa)16/02 17:03
Peakerwhat are costrings?16/02 23:29
Saizanpotentially infinite ones, iirc16/02 23:33
PeakerAgda's compilation is sooo slow. And the agda command line is silly (Can't find its own stdlib without -i... need -i .  to find a file explicitly given..)16/02 23:34
PeakerIt seems Agda has no prelude? or just an extremely limited one?16/02 23:34
Saizanno prelude16/02 23:34
Peakerwhy not?16/02 23:35
Peakerimporting 5 libraries for hello world isn't fun :)16/02 23:35
Saizani don't think putStrLn "Hello World!" is what one'd expect as first agda program16/02 23:36
Peakerheh, it was my first :)16/02 23:37
Peakerall the cool demos of Agda's Nat stuff -- how does it work in practice? Are there hardware-accelerated numbers?16/02 23:37
Saizani believe so16/02 23:38
Peakerdoes some Agda code magically say: "This is the official Nat semantics, but trust me that using this low-level code is equivalent and faster?"16/02 23:38
Saizanperhaps that's what the {-# BUILTIN NAT .. #-} pragma does, in addition to making numeric literals work16/02 23:39
sullythe definition of Nat and its associated functions are annotated with magic comments saying what they are16/02 23:39
sullyso maybe it does that.16/02 23:40
sullyunfortunately Agda is woefully undocumented.16/02 23:40
Saizanthe epic backend should additionally use a BigNum implementation for anything that's isomorphic to Nat after the indices get compiled away16/02 23:41
sullysigh16/02 23:45
sullyI wish things in agda-land were documented.16/02 23:45
Saizanthe release notes are informative16/02 23:46
pigworkerI wish people wouldn't say "Agda is woefully undocumented".16/02 23:56
pigworkerAgda is woefully under-resourced.16/02 23:56
sullyit probably has more resources than SML does at this point, though16/02 23:57
sullysigh.16/02 23:57
pigworkerI'm not so sure about that.16/02 23:57
sullyalthough I suspect this isn't the place to find sympathy about the sad state of my favorite eager and impure language...16/02 23:58
pigworkerExactly. SML's time has gone. It doesn't deserve resource, but...16/02 23:58
--- Day changed Thu Feb 17 2011
sullyyeah, except that I would argue that the world needs a good eager and impure language17/02 00:00
pigworker...SML-style programming is well worth keeping alive, with a tighter type discipline, negociating the deal of which effects are available.17/02 00:00
pigworkerI agree.17/02 00:00
sullyargh, I need to not be on IRC17/02 00:01
sullyI have to finish writing an assignment for CMU's programming languages class17/02 00:01
sullythat needs to go out tomorrow17/02 00:01
PeakerHow does the Epigram effort relate to the Agda effort? Overlapping people or just overlapping interest?17/02 00:02
PeakerIs it really a good idea for Agda, btw, to completely shun away any future hope of reasonable type inference by making name resolution depend on types?17/02 00:02
Peaker(One of my favorite things about Haskell is that name resolution can happen prior to and completely independently from typing)17/02 00:03
Saizanrequiring type signatures for pattern-matching definitions doesn't feel so unreasonable, and you do get inference for the rest, even program inference17/02 00:05
pigworkerEpigram is an always-unstable exploration of things which might become useful Agda functionality at some point. All Epigram hackers are Agda users. Some Agda hackers are Epigram hackers.17/02 00:06
Saizani.e. even computationally relevant values can be inferred if the types are strict enough17/02 00:06
Peakerpigworker, oh, so Epigram is a research sandbox for Agda?17/02 00:08
pigworkernot explicitly, but that has been the main way in which Epigram has had impact17/02 00:09
Peakerone of the cool things about Epigram was the emacs effort, wasn't it? Does Agda have any of that stuff?17/02 00:10
pigworkerthe codebases are completely separate, but then, the Epigram codebase is completely separate from the Epigram codebase, so being separate from Agda is easy17/02 00:10
pigworkerI don't think it was cool that it was emacs (it was really uncool, in fact), but Epigram has much tighter interactivity, for better or worse17/02 00:11
PeakerYeah, text editors suck. We need structural editors. But it seemed like that emacs effort was a step in that direction, at least functionality-wise17/02 00:12
pigworkerSure, but I treated emacs as a curses window I could program in lisp, nothing more. It wasn't pretty. The functionality, rather than the medium, is what's worth keeping.17/02 00:14
PeakerI started work on a structural editor. I realized I needed undo very quickly.  I realized undo/redo is really a special case of revision control.  I diverged a bit to work on a structured transactional revision controlled database as the basis for the structural editor.  Didn't implement merges yet, and had to halt the project in favor of more stressful IBM work (which I will complete soon)17/02 00:15
pigworkerAnd you want Lena Magnusson's local (spatial) undo, rather than temporal undo. Agda simulates this by global-redo.17/02 00:16
PeakerYeah, I want support for local undo too.  I may have chosen an implementation model that makes that a bit difficult17/02 00:17
PeakerThe troubling thing is I consider the code editing part the fun part, and I am not in the fun part yet...17/02 00:18
PeakerI wrote a mostly functional console widget set for this project though (I couldn't find a nice functional UI toolkit to work with)17/02 00:18
pigworkerI'm minded to (a) specify the interface (b) go lower tech. I know how to drive ncurses now.17/02 00:19
Peakerncurses is pretty terrible.. I'd suggest vty instead?17/02 00:20
pigworkerWhat's vty? But I just need vt100-style cursor-moving control codes.17/02 00:21
Peakerwell, if ncurses is ok for what you need, it's probably fine. ncurses just has various artificial limitations (e.g: on number of color pairs, etc).  vty is a mostly-Haskell lib (some C code in there) that does what ncurses does much more elegantly, and with some optimizations that allow you to write nicer code and still have it perform OK17/02 00:22
pigworkerAnything that lets me have cursor movement and my usual five foreground and three background colours will do fine. My first step is to abstract to a treatment of rectangular regions.17/02 00:27
dolioAgda has, what, two and a half people working on it?17/02 00:28
Peakervty has a functional "Image" type that represents a rectangular console area, and you can compose it horizontally/vertically/etc.  I wrapped their image type with one that allows you to compose by overlay too17/02 00:28
dolioI think Epigram has more people. :)17/02 00:28
pigworkeron a good day, with a following wind17/02 00:29
pigworkerEpigram has more people not working on it.17/02 00:29
dolioHeh.17/02 00:29
pigworkerAnd we're keen to grow that number...17/02 00:30
Peakerthen you have something like a Picture type, which is essentially an (Image, cursorPos), and lastly,   update :: Vty -> Vty.Picture -> IO ().    Along with nextEvent :: Vty -> IO Vty.Event     it is a pretty minimal API. Nice, IMO17/02 00:30
pigworkerPeaker: sounds good17/02 00:31
dolioAlso, I can't recall how old Agda's type-directed constructor resolution is, but I'm pretty comfortable with the level of annotation it requires.17/02 00:33
pigworkerI plan to develop an extremely anal-retentive library which associates zippers in the spatial decomposition of your screen with monad homomorphisms from the effects available in a subregion to the effects available in a containing region. Don't hold your breath.17/02 00:33
pigworkerdolio: The deal is pretty much that you get what you pay for. Where is the bad?17/02 00:35
pigworkerThe bad is that type-directed elimination is not so pretty, but perhaps could be.17/02 00:36
dolioI'm mildly under the impression that it changed the level of annotation required not-at-all, but maybe it's the reason all function definitions require an annotation.17/02 00:36
dolioI began thinking that was just the price of dependency.17/02 00:36
Saizansometimes i want to remove things from scope, so that unification gets a problem with a definite solution17/02 00:37
dolioAnd I'm willing ot pay that.17/02 00:37
pigworkerExactly, or rather the price of being allowed to state plans too cranky for a machine to guess.17/02 00:37
doliopigworker: Yeah. I'm rather against the Haskell TNDR proposals. I'm more ambivalent toward Agda's.17/02 00:37
PeakerSaizan, I'm new to this Agda business, but wouldn't that assume a closed-world?  Is unification allowed to assume things out of scope do not exist?17/02 00:38
PeakerTNDR?17/02 00:38
pigworkerWe still do fill-in-the-boring type inference, but we don't do guess what-the-idea-is type inference.17/02 00:38
dolioType-directed name resolution.17/02 00:38
PeakerI think names are just syntactic encodings of the code graph's links, and a good structural editor makes the naming thing moot :)17/02 00:39
Peaker(by editing the code graph directly, rather than an encoding)17/02 00:39
dolioThe Haskell motivation usually strikes me as odd, because it's people desiring ad-hoc overloading in a language that solved that problem elegantly with type classes.17/02 00:39
Peakerdolio, I think it's also the records-arent-a-namespace thing which is different to what everyone's used to17/02 00:40
pigworkerType classes become problematic once application is no longer injective.17/02 00:40
dolioYes, but whenever the issue comes up, people actually want to make TNDR separate from any record proposal, just as an entity in itself.17/02 00:40
pigworkerAnd yes, I want scope resolution to happen before typechecking.17/02 00:40
SaizanPeaker: well, if some x is out of scope then the inference engine had better not use x when it tries to fill in the current term for you, in the cases i was referring to it actually has to take it from somewhere else in fact, and not having x in scope is what removes the ambiguity which allowed multiple solutions17/02 00:42
dolioI tend to take advantage of Agda's overloaded constructors, but I could easily live without them.17/02 00:42
pigworkerI've very much enjoyed the SHE experience of figuring out what's doable by dumb preprocessing, and what takes subtlety.17/02 00:43
PeakerSaizan, ah, so "solutions" are just heuristics you can choose from?17/02 00:43
SaizanPeaker: i'm talking about the level of the implementation of inference, an user just gets told by agda that it couldn't infer the term, and agda inference is a no-guessing one (or should be), if there's more than one possibility it gives up17/02 00:45
pigworkerdolio: in the world of multiple ornaments, overloading constructors is a valuable source of continuity17/02 00:45
Saizans/about/on/17/02 00:47
PeakerSaizan, My only question is by "one possibility" do you mean only one possible term or value that could possibly fill that blank in generality (e.g: only the empty vector for Vector Z A), or only one possible term that's valid given current scope (e.g: only "x" in scope is of a type of the blank)17/02 00:47
SaizanPeaker: in general17/02 00:48
PeakerSaizan, if it's in general, then it shouldn't be affected by scope?17/02 00:48
SaizanPeaker: oh, sure it could, that variable could appear in the types17/02 00:49
dolioAgda's inference can't even guess that there's only one empty vector to fill in a hole in the empty context.17/02 00:49
Saizanmostly because not all empty vectors are automatically equal17/02 00:50
dolioBecause it doesn't know that all Vector Z A are equal to the empty vector.17/02 00:50
dolioThat fact is only provable with induction.17/02 00:51
Peakerwould it be practical for an Agda IDE to search for such proofs in the background as you edit?17/02 00:55
pigworkerer, yes.17/02 00:56
dolioThere is a tool for filling in things more aggressively within the Agda mode.17/02 00:58
dolioI never remember to use it, though.17/02 00:58
Saizanit can even write map for you, apparently17/02 00:58
PeakerI apt-get install'd agda-mode, and I don't even have syntax highlighting.. what gives?17/02 01:10
dolioYou have to load the file to get highlighting.17/02 01:11
dolioConstructors are a different color than projections than coconstructors, etc.17/02 01:11
dolioAlthough there aren't real coconstructors anymore.17/02 01:13
PeakerI have loaded an agda file and got into Agda mode, I believe. something must be broken17/02 01:15
dolioDid you open the file and press C-c C-l?17/02 01:15
dolioOr go to the Agda menu and tell it to load?17/02 01:15
PeakerI'll try, didn't know I had to do that :)17/02 01:16
Peakerah, ioTCM and cmd_load seem missing17/02 01:17
Peakerin the *ghci* buf17/02 01:17
Peakeroh, the module import failed, ok, that's easy17/02 01:17
dolioColors are only known post-type checking, informed by the Agda system.17/02 01:17
dolioExcept comments. I think the mode colors those automatically.17/02 01:17
Peakerthe Agda haskell package doesn't work with GHC 7?17/02 01:19
dolioThe one on hackage probably doesn't.17/02 01:19
dolioThe head does.17/02 01:19
Peaker"darcs get --lazy http://code.haskell.org/Agda" fails with HTTP error?17/02 01:22
Peakerwould be cool if Agda was on git hub?17/02 01:22
dolioYeah, there's a new one after the code.haskell.org hack...17/02 01:22
doliohttp://www.cse.chalmers.se/~nad/repos/Agda/17/02 01:22
djahandariecopumpkin, I want to say I'm 1/2 done ;) But it's so long already :(17/02 05:26
copumpkin?17/02 05:27
lambdabotcopumpkin: You have 1 new message. '/msg lambdabot @messages' to read it.17/02 05:27
djahandarieThe little piece I'm writing on that code17/02 05:27
copumpkinoh17/02 05:28
copumpkindon't credit me with it, it certainly isn't my idea :P17/02 05:28
copumpkinnot sure whose it is though17/02 05:28
djahandarieI plan on mentioning you, I know you didn't come up with the idea though :)17/02 05:29
djahandarieEnjoy the fame while you can17/02 05:29
copumpkinhah okay17/02 05:29
glguy_total x x' != w of type x ≤ x' ⊎ x' ≤ x17/02 08:47
glguy_when checking that the expression17/02 08:47
glguy_lem1 {z} (_∷_ {_} {_} x xs) (_∷_ {_} {_} x' xs') has type17/02 08:47
glguy_(x : Any (_≡_ z) (x ∷ xs)) →17/02 08:47
glguy_Any (_≡_ z) (merge (x ∷ xs) (x' ∷ xs') | w | merge xs (x' ∷ xs'))17/02 08:47
glguy_Could someone help me understand this message?17/02 08:47
glguy_I'm confused because total x x'     Have: x ≤ x' ⊎ x' ≤ x17/02 08:47
glguy_and the function I'm trying to learn more about branches based on the value of total x x'17/02 08:50
glguy_It's late, so I'm going to head to bed, but my other client will be online (glguy) for me to see any responses in the morning17/02 08:52
Saizanlooks like a with bug17/02 09:30
PeakerAgda sources seem like they have lots of unqualified open imports :-(17/02 10:34
PeakerI darcs-got Agda, and used the agda-mode within it (src/data/emacs-mode), and it seems there are no errors in the *ghci* buffer, but I still don't get any colors17/02 11:10
Saizan*Agda information* ?17/02 11:19
PeakerI don't know have that buffer17/02 11:21
djahandariePeaker, you need to load the code to get the highlighting17/02 16:42
djahandarieC-c C-l, I think :P17/02 16:43
copumpkindolio: was it monoidal categories that used too much memory in your attempt?17/02 18:31
copumpkinhmm, probably17/02 19:01
copumpkinhmm, I suppose my functors should respect the underlying categories' equality17/02 20:24
copumpkinI wonder if that follows from the other functor laws, actually17/02 20:26
copumpkindon't think so17/02 20:26
doliocopumpkin: No, it was merely various proofs about products.17/02 20:51
dolioAssociativity and commutativity up to isomorphism.17/02 20:51
copumpkinah okay17/02 20:52
copumpkinI'll have to play with that and see if this representation uses less memory (I use irrelevance wherever possible)17/02 20:52
copumpkinor did you already try your stuff with irrelevance?17/02 20:52
dolioNo, I stopped working on it before the irrelevance stuff hit.17/02 20:52
copumpkinokay17/02 20:53
* copumpkin trembles17/02 21:20
copumpkindoing commutativity17/02 21:20
dolioAssociativity is way worse.17/02 21:24
copumpkinI imagine :P17/02 21:25
copumpkinit's just a real pain not being able to use propositional equality17/02 21:25
copumpkineverywhere I look I want to use subst17/02 21:25
dolioAre you using preorder reasoning yet?17/02 21:27
copumpkinI was going to, but my issue is that my equality is parametrized implicitly by the objects17/02 21:28
copumpkinso it doesn't quite fit into a single setoid/preorder17/02 21:28
copumpkinI can basically make a preorder for all pairs of objects17/02 21:28
dolioThat doesn't sound any different than the situation I had.17/02 21:29
copumpkinfair enough17/02 21:29
copumpkinI still see you using cong in your products thing17/02 21:30
copumpkinI'm not sure I get that?17/02 21:30
doliohttp://hpaste.org/44095/commutativity_of_the_product_f17/02 21:31
dolioDid that get through?17/02 21:34
copumpkindolio: neat, but wouldn't you want to do that for a specific pair of products?17/02 21:34
copumpkinyeah17/02 21:34
dolioThis was in the Has-Products record.17/02 21:35
copumpkinyeah17/02 21:35
copumpkinI mean even if you don't have all products, if you have a pair of products AxB and BxA, you can do this17/02 21:35
dolioAnyhow, I only appear to use cong to prove that if g = h, then f . g = f . h.17/02 21:36
copumpkinI see17/02 21:36
copumpkinI can get that easily from my composition respects equality17/02 21:36
dolioWhich should be true for any category, hopefully.17/02 21:36
copumpkinmind if I steal your proof then?17/02 21:36
dolioGo ahead.17/02 21:36
copumpkinthanks!17/02 21:36
dolioI can paste associativity, too, but it's more than twice as long.17/02 21:36
dolioMaybe 3x.17/02 21:36
copumpkinI'll set up the preorder machinery first17/02 21:37
copumpkinsure17/02 21:37
copumpkinI'm going to try to do it for specific products and then make the "has binary products" version call the specific version17/02 21:37
doliohttp://hpaste.org/44096/assocativity17/02 21:39
dolioThere's associativity. I thought I was annotating, but apparently not.17/02 21:39
copumpkinI can see why agda might get rather slow with that :)17/02 21:40
dolioOr, maybe annotations don't appear on the same page anymore.17/02 21:40
dolioYeah, I haven't loaded all this in a while, but it used to take more than half of my memory.17/02 21:40
dolioAnd it probably takes between 5 and 10 minutes to load.17/02 21:41
copumpkinwow :P17/02 21:41
copumpkinI wonder if it's minimal17/02 21:41
copumpkindo I get anything for free by providing a setoid of arrows instead of a preorder of them?17/02 21:41
dolioHowever, those huge proofs should be able to be irrelevant, I think.17/02 21:41
copumpkinI'd think so17/02 21:42
dolioArrows of a category are supposed to be a set.17/02 21:42
dolioUnless it's an enriched category.17/02 21:42
copumpkinI guess I might as well, because I have an equivalence class anyway17/02 21:42
dolioSo setoid is the right thing for them to be.17/02 21:43
dolioOtherwise you can maybe have multiple identity arrows that are isomorphic but not the same.17/02 21:43
copumpkinyeah17/02 21:44
copumpkinoh, irrelevance makes my setoid less than ideal17/02 21:45
copumpkinmaybe the Relation.Binary Setoid should have an irrelevant IsEquivalence17/02 21:45
copumpkinotherwise I need to make my entire setoid irrelevant17/02 21:46
dolioisEquivalence could probably be irrelevant, yes.17/02 21:48
doliois the library even taking advantage of that?17/02 21:48
dolioThe standard library, that is.17/02 21:48
dolioI thought irrelevance might still be too controversial.17/02 21:48
copumpkindoesn't look like it17/02 21:48
* copumpkin sighs17/02 21:48
copumpkinyeah17/02 21:48
copumpkindammit17/02 21:48
copumpkinmaybe I should divorce from the standard library entirely17/02 21:48
copumpkinit's not like I use mucho of it anyway17/02 21:48
copumpkinwow, very hispanic of me17/02 21:49
copumpkinthen I could stop avoiding its ownership of Category17/02 21:49
dolioSounds like a win-win situation. :)17/02 21:49
copumpkinhell yeah17/02 21:50
copumpkinI wonder if I can make a "truer" category of sets by using A -> Set17/02 21:50
copumpkinI guess I'll explore that later17/02 21:53
dolioI'm not sure what you mean by that.17/02 21:53
dolioIf you're referring to the complaint a few days back that Agda's set lacks some things from the set theoretic set...17/02 21:54
dolioLike, say, pushouts...17/02 21:54
copumpkinyeah17/02 21:54
dolioThen the right solution to that is to make a category whose objects are Setoids.17/02 21:54
copumpkinhmm, fair enough17/02 21:54
dolioBecause Setoids can represent quotients.17/02 21:54
copumpkinyeah17/02 21:54
dolioI think that's the only thing really missing.17/02 21:57
copumpkinI was wondering about a subobject classifier17/02 21:57
dolioWell, there are other things missing, but they're controversial.17/02 21:57
copumpkinwould a Sigma do that?17/02 21:57
copumpkinI've made a subobject classifier in my library, but haven't tried instantiating it yet17/02 21:57
dolioNo. Set/Prop is the subobject classifier, but it's not in-universe.17/02 21:58
copumpkinso that seems like another thing that would be nice to have17/02 21:58
dolioPowersets are impredicative, generally.17/02 21:58
copumpkinwhat I meant by my "truer" category of sets before was taking the stuff from here: http://www.cse.chalmers.se/~nad/listings/lib/Relation.Unary.html#117/02 21:58
dolioWell, that would be about the poset category of subsets of a given set, which is another matter.17/02 21:59
copumpkinI guess17/02 22:00
copumpkinyeah, I already have a thingy that builds a category from a preorder17/02 22:00
dolioThe Setoid category would also lack choice, of course, but that's also controversial.17/02 22:00
copumpkinhow about the categorical constructs that rely on functors to set?17/02 22:00
copumpkinI'd just have to cross my fingers that none of them rely on stuff that our "category of agda sets" doesn't support?17/02 22:01
copumpkinor agda setoids17/02 22:01
dolioProbably, I guess.17/02 22:01
copumpkinAgda-Representable and Setoid-Representable17/02 22:02
copumpkinmaybe17/02 22:02
* copumpkin shrugs, will think about it after rearranging17/02 22:02
--- Day changed Fri Feb 18 2011
copumpkinso if I'm ditching the standard library, where should I keep the couple of pieces I need? I want dependent products (with and without irrelevant snds) and non-dependent products (separate is nice), and I want equivalence relations and setoids (and the setoid reasoning trick)18/02 02:33
copumpkin(setoids with irrelevant equivalence relations)18/02 02:34
copumpkinit seems weird to give the modules the same names18/02 02:34
dolioI usually dump them all in a single file because I'm too lazy to make a proper library structure.18/02 02:40
dolioWith a name like Meta or Basic or something.18/02 02:40
copumpkinfair enough :)18/02 02:40
copumpkinit'll do for now18/02 02:40
copumpkinah, I see why NAD may not have added irrelevance18/02 05:28
copumpkinit breaks all the nice module exposing stuff he has in all his structures18/02 05:28
copumpkinall of them open subparts publicly18/02 05:28
copumpkindolio: my commutativity proof ended up being quite a bit smaller than yours18/02 19:39
copumpkinnot sure if I messed up one of my properties18/02 19:39
copumpkinnow for associativity18/02 19:42
dolioCategory.Product just spent 20 minutes type checking before I killed it.18/02 22:46
dolioUsed 1 GB of my swap.18/02 22:46
doliocopumpkin: So, why is your proof shorter? Is it the different definitions for some of the product properties?18/02 22:47
dolioI tried to stick as close as possible to the usual category theoretic definitions, but it's entirely possible that those are sub-optimal from a, "we're writing out proof terms in exquisite detail," perspective.18/02 22:48
dolioOf course, maybe I just missed something back when I wrote them.18/02 22:50
copumpkindolio: well, I still haven't done assoc :) been half proving, half watching talks at a symposium18/02 22:50
copumpkindoes commutative still take loads of memory?18/02 22:50
dolioProbably. I don't really feel like checking right now. My computer is still recovering.18/02 22:51
copumpkinbut I think what I did would work with yours too18/02 22:52
copumpkinhttp://hpaste.org/44122/commutative_product18/02 22:52
copumpkinplease ignore the horrible module structure18/02 22:53
copumpkinI plan on rethinking that later, but I'm more interested in writing proofs for now18/02 22:53
copumpkinbut I use irrelevance everywhere I can, so I'd hope it'd be a bit lighter on the memory18/02 22:54
copumpkinoh and I also have http://snapplr.com/02zm18/02 22:56
dolioI'm not sure I see how your proof actually works...18/02 22:58
dolioHow does 'sym (p1.universal ...)' apply to swap . swap?18/02 22:59
copumpkinlet me take out the _18/02 23:00
copumpkin         ≈⟨ sym (p₁.universal π₁ π₂ (⟨ π′₂ , π′₁ ⟩ ∘ ⟨ π₂ , π₁ ⟩′) (p₁.commute₁ π₁ π₂) (p₁.commute₂ π₁ π₂)) ⟩18/02 23:03
dolioOh, the swap . swap is the i I guess.18/02 23:03
copumpkinI'm gonna leave it like that actually18/02 23:03
copumpkin_ are useless18/02 23:04
dolioWait a minute...18/02 23:04
* copumpkin trembles18/02 23:05
dolioThat specification of universal looks wrong.18/02 23:05
dolioThere's no conditions on i.18/02 23:05
copumpkinokay, that might explain what's wrong then :)18/02 23:05
copumpkinbah :)18/02 23:05
copumpkinyou're right18/02 23:05
dolioDid I forget those, too?18/02 23:05
copumpkinno18/02 23:06
dolioOkay.18/02 23:06
copumpkinI screwed up my translation of your Commutes thing18/02 23:06
copumpkin               → π₁ ∘ ⟨ f , g ⟩ ≡ f18/02 23:06
copumpkin               → π₂ ∘ ⟨ f , g ⟩ ≡ g18/02 23:06
copumpkinthose are trivial18/02 23:07
* copumpkin goes back and fixes everything :(18/02 23:07
dolioNo, I did leave that out.18/02 23:07
dolioOh, wait. No.18/02 23:07
copumpkinyou have              → Commutes i π₁ f → Commutes i π₂ g18/02 23:07
dolioOkay, right.18/02 23:08
copumpkinso basically with my definition I could always "feed" universal commutes1 and commutes218/02 23:08
dolioRight.18/02 23:08
copumpkinand that's what I was doing to get my easy proofs :)18/02 23:08
copumpkinboo18/02 23:08
dolioThat probably explains your different eta, too.18/02 23:08
copumpkinyep18/02 23:08
copumpkinit broke now18/02 23:08
dolioI guess I should have noticed that.18/02 23:08
copumpkinah well, I still hope memory usage will be smaller, even if the proofs are the same18/02 23:09
copumpkingiven the irrelevance18/02 23:09
copumpkinnot sure if native equality would use more or less memory though18/02 23:09
dolioYeah. I don't know how exactly that's handled.18/02 23:09
dolioBut if it throws out irrelevant stuff more aggressively, that can only be good.18/02 23:09
copumpkinyeah18/02 23:09
copumpkinI think an equivalence relation might hurt me a bit memorywise18/02 23:10
dolioI'm not totally sure why this all takes so much memory, really.18/02 23:11
dolioI mean, those proofs are obviously big.18/02 23:11
copumpkinyeah18/02 23:11
dolioBut, like, 2 - 3 GB big?18/02 23:11
copumpkinyeah, seems weird18/02 23:12
copumpkinanyway, I'll fix these proofs tonight, batt running out now18/02 23:12
copumpkinthanks for the help18/02 23:12
dolioSince it's all a composition of functions that look like 'foo refl refl = refl'. :)18/02 23:12
dolioAnd opaque hypotheses.18/02 23:13
Saizani wonder if when one metavariable gets solved its value just gets put directly into the AST or if there's an explicit graph structure kept around18/02 23:14
dolioI've never gotten the energy up to really look at Agda's internals.18/02 23:15
dolioOf course, I have no doubt the interpreters I've written would blow up at examples of that size.18/02 23:17
dolioWere they even sophisticated enough to handle them.18/02 23:17
--- Day changed Sat Feb 19 2011
dolioYou know, my computer was running for hours with .7 GB of swap usage after trying to load that product file.19/02 01:07
dolioAnd I have the kernel set to minimize swap usage.19/02 01:07
dolioMakes me wonder what my memory is actually being used for.19/02 01:08
djahandarieI just turned off my swap entirelly19/02 01:46
djahandarieswapoff!19/02 01:46
djahandarieBecause when I swap it's a lot worse than the OOM killer19/02 01:47
djahandarieWhat is the actual definition of "inhabitant"? I only hear it thrown around casually19/02 05:31
dolioI would say an inhabitant of X is a closed term of type X.19/02 05:38
dolioBut it might depend on context.19/02 05:39
dolioIt's the same idea as 'element' only more specific to constructive type theory.19/02 05:40
djahandarieAlright, thanks. Basically what I had grokked from hearing it used.19/02 05:41
dolioWhere people talk about types being 'inhabited' to suggest a constructive property of their containing elements.19/02 05:41
dolioIn set theory, people say 'non-empty,' but that's more like a double-negative, which is not equivalent to a (strict) positive in intuitionism.19/02 05:42
djahandarieA constructive property?19/02 05:42
dolioLike, "I can give an example of an element."19/02 05:42
dolioVersus, "if I assume there are no elements, I can derive a contradiction."19/02 05:42
djahandarieOkay, cool.19/02 05:42
djahandarieIs there a word for value/type in Agda? i.e., anything19/02 05:47
djahandarieOr am I just allowed to say types are values?19/02 05:47
dolioTerm?19/02 05:47
djahandarieAh, right. :o)19/02 05:48
djahandarie(Trying to find the proper language to use in this thing I'm writing)19/02 05:48
starcloudedhello everybody19/02 16:47
copumpkinhi19/02 16:48
starcloudedwhat are the monads?19/02 16:49
copumpkinum19/02 16:59
copumpkinthey are abstract structures in category theory, that are a fairly common codified "design pattern" in haskell19/02 16:59
freiksenetthat's even more epic than "what is curry howard isomorphism in two words"19/02 17:01
freiksenet:)19/02 17:01
freiksenetno offense :)19/02 17:01
copumpkin"no offense" is what the curry-howard isomorphism is, in two words? :P19/02 17:02
copumpkinmonoid object in category of endofunctors and haskell design pattern encoding DSLs with variable binding19/02 17:03
freiksenetthey are also burritos19/02 17:05
copumpkinalso, just a lax 2-functor from the terminal bicategory, duh19/02 17:06
freiksenetthis guy is funny :)19/02 17:07
dolioMonad are just monads in the 2-category of categories.19/02 17:07
copumpkinlooks like we lost him19/02 17:08
freiksenetcopumpkin: he is funny. last time he popped in and asked "can someone explain me what curry-howard isomorphism means"19/02 17:09
copumpkinoh :)19/02 17:09
dolioI thought you'd just made that up.19/02 17:10
freiksenetno, that's why I was so amused.19/02 17:10
copumpkinwell, it's a valid question in here :)19/02 17:11
kulakowskifreiksenet: I saw that, it was amusing19/02 17:13
freiksenet12:02:38 starclouded | anyone could explain to me in a few words the Curry-Howard isomorphism?19/02 17:14
freiksenethere is exact quote19/02 17:14
copumpkin"types are logical statements"19/02 17:14
kulakowskicopumpkin: I think he was told "proofs are programs" or vice versa19/02 17:14
copumpkin"type is logic" ?19/02 17:14
copumpkinah19/02 17:14
freiksenetyeah, that's what I said19/02 17:14
dolioIt doesn't take that many words if you don't want much real understanding.19/02 17:16
dolioPropositions as types, programs as proofs.19/02 17:16
freiksenetdolio: yeah. I just don't see real point of asking this kind of questions. you need to read on it yourself and then, if you don't get something, ask about it. just popping out and asking to explain a complex abstract concept won't get you closer to understanding19/02 17:19
dolioYeah.19/02 17:20
Saizanfreiksenet: maybe the best answer is a link to a good reference then19/02 17:21
freiksenetSaizan: true.19/02 17:22
Saizannice, switching from a 7-nested sigma type to a custom record made typechecking time reasonable again19/02 17:34
Saizangoing from 1.6G to 0.7G of memory used..19/02 17:36
dolioWow, really? That's a dramatic improvement.19/02 17:36
Saizanyeah, i wish i had committed the old version to the repo, now i've to manually revert to check again19/02 17:40
Saizanhttp://hpaste.org/44138/sigmas_vs_custom_record <- long story short: 45s 1200MB vs. 9s 400MB19/02 18:02
Saizandarcs version of Agda, on a 64bit machine19/02 18:02
* glguy idly wonders about having more than two levels relevant and irrelevant19/02 19:09
glguy"dolio: Monad are just monads in the 2-category of categories."19/02 20:55
djahandarie@remember dolio Monad are just monads in the 2-category of categories.19/02 21:45
lambdabotIt is forever etched in my memory.19/02 21:45
djahandariepigworker, re: turing-complete, wouldn't not typechecking the corecursion be completely subverting the type system? More like unsafeCoerce than IO.19/02 21:50
* Saizan wonders what that is in reply to19/02 22:03
djahandariehttp://www.reddit.com/r/haskell/comments/fmp66/i_have_yet_to_learn_a_functional_programming/c1h2r7a19/02 22:03
Saizannot unfolding /= not typechecking19/02 22:05
djahandarieHow do you check it at all without unfolding it?19/02 22:06
Saizanyou typecheck the expression that's supposed to produce it19/02 22:06
Saizanlike you typecheck ones = 1 : ones without creating an infinite list19/02 22:06
Saizanit'd be problematic if e.g. you wanted to create a type by looking at the last element of ones19/02 22:07
Saizanbut that wouldn't pass the productivity checker19/02 22:07
djahandarieHmm, I see19/02 22:08
--- Day changed Sun Feb 20 2011
pigworkerdjahandarie: it is perfectly normal that you do not have to run a program to typecheck it; it is perfectly normal that Turing-complete languages have typecheckers which do not execute general recursive programs statically; Agda is no exception, except in that typechecking Agda does involve running some programs statically20/02 00:29
djahandarie"Some, but not all programs" being the point here I guess.20/02 00:32
pigworkerRight. It's a novelty that you can persuade the typechecker to run programs at all; this does not inhibit the run time runnable programs.20/02 00:34
dolioAgda has no built-in facility for run-time running Turing complete programs, either, though.20/02 00:39
ccasindoes Agda even have a particularly well-explained facility for running programs at all?20/02 00:40
dolioThen again, I'm not really sure what facility it has for runtime at all, since I've never compiled anything.20/02 00:40
ccasin:)20/02 00:40
pigworkerIt's a fair point that a lot more attention is paid to the operational semantics used to interpret Agda programs statically. The runtime behaviour is up for grabs. A delay monad interpreted by general recursion at runtime is entirely feasible.20/02 00:49
ccasinYes, it's definitely easy to imagine ways to evaluate agda programs (including ones with corecursion)20/02 00:53
Saizanone problem is see with the delay monad is that for efficiency you don't want to construct the intermediate "Step" constructors, though that representation is handy when you want to prove termination for some special case20/02 00:54
ccasinthough the lack of rules here is a little concerning - can we come up with evaluation strategies that disagree with the static equality?20/02 00:54
pigworkerThe right comparison is between Agda's static semantics and, say, C++'s template language.20/02 00:55
ccasinprobably any deterministic strategy will disagree on some programs that the typechecker says are equal20/02 00:56
pigworkerSaizan: there's no need for those step-constructors to manifest at runtime, if we have a call-by-need semantics; step-constructors might even help give a mostly call-by-value semantics; they might correspond to thunking, but not to gratuitous boxing.20/02 00:59
ccasinpigworker: the template language analogy is interesting, but I think it misses something.  Since Agda's static semantics is concerned with the same expressions as its dynamic semantics, there is a risk of disagreement here.  On the other hand, templates are clearly a separate part of the C++ language20/02 00:59
ccasinI'm just rambling now, though20/02 01:00
pigworkerAgda fools you into thinking you can make the typechecker do any old shit. Then it turns out the typechecker wan't born yesterday. Dynamically, who cares?20/02 01:01
pigworkerTurns out, in C++, you can make the typechecker do any old shit.20/02 01:02
dolioI might care if the static proofs about my dynamic programs don't match the dynamic semantics.20/02 01:02
dolioIf we're just doing any old thing.20/02 01:02
ccasinYes, I agree - with coinduction, the typechecker can't see as much as we can observe dynamically, and that's fine20/02 01:03
pigworkerYou want a guarantee that the static semantics underapproximates the dynamic semantics.20/02 01:03
ccasinright - it would be weird if we could prove two programs equal but one diverges and one doesn't20/02 01:04
ccasinwhich might happen if we did CBV evaluation on agda programs20/02 01:04
pigworkeryou should be able to do CBV except for "musical" delays20/02 01:05
Saizanpigworker: assuming we prevent somehow that the number of step constructors becomes computationally relevant20/02 01:06
pigworkerSaizan: I assume no such thing. It gives a more accurate model of current non-total practice to prevent the counting of delay steps, but what makes that current practice worth modelling at that accuracy? This way, we argue about the accuracy of the model, not its existence.20/02 01:10
ccasinpigworker: I guess so (if I understand "musical").  I just meant to point out that specifying the runtime behavior of agda programs isn't trivial and is disappointingly ignored20/02 01:11
pigworkerI agree. edwinb thinks about these things more than the rest of us, but he could use a friend.20/02 01:13
Saizani guess i'm just worried that supporting the counting of delay steps would induce a lot of overhead at runtime20/02 01:15
Saizanyou could implement parallel or with such a thing though20/02 01:16
pigworkerYeah. But it should be possible to quotient away from that awareness.20/02 01:19
pigworkercripes! is that the time? bed time!20/02 01:22
copumpkindjahandarie: hey, I was just watching conor's summer school videos on the train20/02 04:48
copumpkinand it covers the STLC very nicely and does lots more too20/02 04:48
copumpkinyou should watch them if you haven't already20/02 04:48
djahandarieI haven't, I'll do that. Do you have a link?20/02 05:02
copumpkinhttp://www.cs.uoregon.edu/Activities/summerschool/summer10/curriculum.html20/02 05:04
copumpkinloads of yummy stuff on there20/02 05:04
djahandarieOh that! I've seen part of the first one I think20/02 05:06
copumpkinthat one's in haskell, but good too20/02 05:06
copumpkinthe others are all agda20/02 05:06
copumpkinand he builds an STLC eventually20/02 05:06
copumpkinincluding a typechecker for it20/02 05:06
glguy∀ {A B C D : Set} → A ⇿ B → C ⇿ D → (A ⊎ C) ⇿ (B ⊎ D)20/02 05:06
glguyIs this already proven via a library function I'm missing?20/02 05:07
glguyLooking at Function.Inverse20/02 05:07
copumpkinI haven't seen it before20/02 05:07
djahandariecopumpkin, wasn't there Epigram stuff in the first one? Or was that another video...20/02 05:07
glguyI'm building it out of Function.Inverse.zip at this point, closest match I found20/02 05:07
copumpkindjahandarie: nope it was all agda + SHE20/02 05:07
djahandarieOh, it was SHE, yeah20/02 05:08
copumpkinI mean haskell + SHE20/02 05:08
copumpkinin his last talk he talks about the ornamental algebras stuff, too20/02 05:08
copumpkintime to fix my proofs and move on!20/02 16:31
copumpkinand by my proofs, I mean my corruptions of dolio's proofs ;)20/02 16:31
copumpkindolio: hmm, your eta uses a cong that isn't about composition20/02 16:37
copumpkindolio: oh, but I think I did find a simpler proof of eta20/02 16:43
copumpkinokay, fixed commutativity20/02 17:12
copumpkinstill low memory consumption for no20/02 17:23
copumpkinw20/02 17:23
copumpkinooh new agda release on cabal20/02 17:34
copumpkinlooks like irrelevant projections are on by default now20/02 17:40
copumpkinand the option is gone20/02 17:40
copumpkinit'd be nice to have special keys for adding steps to equational/preorder reasoning sequences20/02 18:28
copumpkinman, making a bunch of inferrable arguments implicit has made my life so much easier20/02 19:21
glguyThe RingSolver would be so cool if it was usable on computers that existed today20/02 19:53
Saizanmaybe if it was compiled..20/02 19:54
copumpkinglguy: you want too much! :P20/02 19:54
glguy    ( z ∈ [ y ] ⊎ z ∈ xs  ⊎ z ∈ ys) ⇿⟨ {!solve 3 (λ a b c → a :+ b :+ c := b :+ (a :+ c)) ? ? ? ?!} ⟩20/02 19:55
glguy    (z ∈ xs ⊎ (z ∈ [ y ] ⊎ z ∈ ys))20/02 19:55
glguyso close!20/02 19:55
copumpkinwhat are you working on? :o20/02 19:55
Saizansort functions?20/02 19:55
glguyyeah, I was toying with a merge and showing that it was a permutation of xs++ys and that it sorted, and that any two sorted lists according to my dectotalorder which were permutations of each other were equivalent up to the dectotal order's ==20/02 19:56
glguyMostly I'm playing with the Function.Inverse namespace at this point20/02 19:56
glguyhttp://www.galois.com/~emertens/inv-merge/embedded-merge.html20/02 20:22
glguyhttp://www.galois.com/~emertens/inv-merge/embedded-merge.html#264320/02 20:23
glguyFinally got this definition (right-step) to load :)20/02 20:23
copumpkincodolio: final tally, takes 30 seconds to typecheck and 550 MB, with pairwise assoc and comm, as well as the same thing on all binary products20/02 20:25
copumpkinalmost identical proof structure to yours20/02 20:25
copumpkinbut with more ugliness to deal with the fact that I don't get all binary products up front20/02 20:26
copumpkinanyone here going to hac phi?20/02 20:41
starclouded_hello everybody20/02 20:47
copumpkinhi20/02 20:48
copumpkinand I have functor composition too now20/02 21:15
doliocopumpkin: That certainly seems like an improvement.20/02 22:01
dolioAlthough, I do wonder a little if having the proof be for all products instead of a particular pair provides some benefit.20/02 22:02
dolioBut there are too many other factors.20/02 22:02
copumpkin?20/02 22:02
copumpkinhow do you mean?20/02 22:02
dolioI mean, does it take more or less memory for 'forall A B -> A x B ~ B x A' compared to 'AxB ~ BxA'?20/02 22:04
copumpkinoh20/02 22:05
copumpkinI haven't tested it20/02 22:05
copumpkinand no way in hell I'm rewriting all that stuff now :P20/02 22:05
dolioExactly.20/02 22:05
dolioI was going to ask how big a difference irrelevance makes, too, but you'd have to tweak 5 different files, probably.20/02 22:05
copumpkinyeah, I guess there are three things different in my version from yours20/02 22:06
copumpkinI'd still bet irrelevance is the single largest factor20/02 22:06
copumpkinbut not sure how much the other two play a role20/02 22:06
copumpkindo exponentials work the same way?20/02 22:07
copumpkinI mean, is it meaningful to talk about the exponential of two particular objects as if others may not exist?20/02 22:08
copumpkinI don't really hear "exponential" vs. "all exponentials" as much as "product" and "all products"20/02 22:08
dolioYes, I think so. Except you can't use the definition via adjunctions.20/02 22:08
dolioThat's a general problem.20/02 22:08
copumpkinI've been aiming for the simple definitions everywhere, with separate proofs showing how to get from one thing to another20/02 22:09
dolioProducts can be defined via adjunction, but only if all products exist.20/02 22:09
dolioFor exponentials, it's (A x -) -| (A -> -), but that means A -> B exists for all B.20/02 22:10
dolioAnd A x B must exist for all B, too.20/02 22:10
copumpkinyeah20/02 22:11
copumpkinhmm20/02 22:11
copumpkinthe ctfp version bothered me because they don't make a natural isomorphism between the curried and uncurried versions20/02 22:12
copumpkinwhich I guess is just wrong, since you only get one of uncurry or curry (can't remember which direction they went in)20/02 22:12
copumpkinI dunno20/02 22:12
dolioActually, I guess (- x A) -| (A -> -) is arguably nicer.20/02 22:13
dolioThat way you get (X x A) -> Y ~ X -> (A -> Y)20/02 22:13
dolioThe usual way is weird.20/02 22:14
dolioIt's curry and flip combined.20/02 22:14
copumpkinyeah20/02 22:14
copumpkinhmm20/02 22:14
dolioOn the other hand, that leads to the S -> (A x S) state monad, which is disliked.20/02 22:15
copumpkinwell, I'm going to define it naively to begin with anyway20/02 22:15
dolioAnyhow, one of the other definitions on wikipedia may help you define exponentials without adjunctions, and thus without all products.20/02 22:16
dolioPeaker: Hah, you could have just waited a couple days. There's a new release of Agda on hackage. :)20/02 23:18
dolioWow, Ulf made a change that halved the memory requirement for checking the standard library.20/02 23:21
copumpkinoh nice20/02 23:22
copumpkinI wonder if I have that change or not20/02 23:22
copumpkinand whether that also affected the products20/02 23:22
dolioI assume that means checking Everything.agda20/02 23:22
dolioIt has to do with importing modules multiple times.20/02 23:23
dolioSo I suspect not.20/02 23:23
copumpkinoh ok20/02 23:23
dolioAnd unless you've rebuilt after the 18th...20/02 23:24
* Saizan wonders how it compares wrt time20/02 23:25
dolioAnd darcs seems to be hung on the version bump patch...20/02 23:25
copumpkinugh20/02 23:51
copumpkinI wish goals would display with the renamings I've done to modules in scope20/02 23:51
copumpkinrather than the full projection syntax20/02 23:51
copumpkinhttp://snapplr.com/qhe220/02 23:51
copumpkinthat's actually fairly clean after doing it right20/02 23:51
copumpkinwell, cleaner, anyway20/02 23:55
copumpkin∀ {A B} (f : C.Hom A B) → ((I₁ (X.η B) ∘E Y.η (F₀ B)) ∘E H₁ (F₁ f)) ≡E (I₁ (G₁ f) ∘E (I₁ (X.η A) ∘E Y.η (F₀ A)))20/02 23:56
copumpkin:(20/02 23:56
--- Day changed Mon Feb 21 2011
npouillardcopumpkin: worse than full projection syntax is when big values (records here) are inlined in my face http://paste.pocoo.org/show/TEXzf7wtp6FTAjPasDUj/21/02 00:14
copumpkinouch :(21/02 00:14
copumpkinyou can ask that thing not to normalize values for you21/02 00:14
copumpkinbut that might be ugly too21/02 00:14
npouillardusing what? 'abstract'21/02 00:15
copumpkinthere's some flag in agda-mode21/02 00:15
copumpkinI can't remember what it is21/02 00:15
copumpkinw00t21/02 00:22
copumpkinI just built both horizontal and vertical composition of natural transformations21/02 00:22
copumpkinone of them was rather hairy :P21/02 00:23
copumpkinat least by my standards21/02 00:24
copumpkinI should probably prove that functor composition has an identity and is associative, and then do the same for both NT compositions21/02 00:27
copumpkinmaybe I'll do that later when I make categories out of them21/02 00:28
copumpkin_ != _ of type21/02 00:39
npouillardcopumpkin: are they irrelevant ?21/02 00:41
copumpkinyeah :P21/02 00:41
copumpkinactually, not these21/02 00:41
npouillardoops then21/02 00:41
copumpkinproj′₁ _ ≡ proj′₁ _21/02 00:47
copumpkin:(21/02 00:47
copumpkinthat's my goal21/02 00:47
copumpkinnot really sure how that happened21/02 00:50
copumpkinmust be some irrelevance where it doesn't belong21/02 00:50
copumpkinoh, and indeed it is :)21/02 00:51
copumpkinmy sigma accidentally had an irrelevant proj221/02 00:51
copumpkindolio: this arrow category takes up more memory than the product proofs :/21/02 00:52
* copumpkin wonders how deadly it would be to try the arrow category of the arrow category of the arrow category21/02 00:52
npouillardcopumpkin: if its not deadly enough I'm pretty sure you can iterate the process21/02 00:54
copumpkin:P21/02 00:54
copumpkinthe arrow of the slice of the arrow of the arrow of the slice of the arrow21/02 00:56
npouillardcopumpkin: will your dev a good way to learn (better) category theory?21/02 00:58
copumpkinnot sure about learning, but it's a lot more explicit about certain aspects of category theory that are often glossed over :) and I'm going to try to keep the thing fairly clear (and eventually will include diagrams in comments)21/02 00:59
npouillardnice21/02 01:00
copumpkinI've put some stuff up at https://github.com/pumpkin/categories21/02 01:32
npouillardcopumpkin: thanks21/02 01:36
copumpkinmost of the files in there are just placeholders for now21/02 01:36
doliocopumpkin: That's difficult to believe. What is using it all?21/02 01:47
copumpkindolio: beats me :/ you're welcome to try it21/02 01:47
dolioComposition of commutative squares or something?21/02 01:47
copumpkinthat is the longest proof in the file21/02 01:54
copumpkinso I'd probably blame it on that21/02 01:54
copumpkinI wonder what it'd take to get cabal working on agda files and what it'd mean to "install" an agda library21/02 01:59
copumpkinI'll happily accept patches for that repository by the way21/02 02:00
copumpkinif anyone finds anything wrong or wants to rework stuff21/02 02:00
doliocopumpkin: I think I'm going to have a hard time writing an arrow category unless I start using irrelevant stuff, which my old category theory stuff doesn't.21/02 02:02
copumpkinhow do you mean?21/02 02:03
dolioOtherwise I have to prove that certain proofs are equal, which is probably impossible.21/02 02:03
copumpkinit just takes a category and gives you another category21/02 02:03
dolioWell, maybe not, due to K.21/02 02:03
copumpkinoh I see what you mean21/02 02:04
dolioCommutative squares carry a proof.21/02 02:04
copumpkinto test memory usage of the same thing in your library21/02 02:04
copumpkinyeah21/02 02:04
copumpkinI'm thinking of un-parametrizing all my modules21/02 02:05
copumpkinsince it makes certain things really ugly21/02 02:05
dolioAll right, I think I decided I don't want to do this. :)21/02 02:28
copumpkinyou're welcome to just add to this library :D21/02 02:28
dolioWell, I think I can actually complete it here, using K.21/02 02:29
dolioI just don't want to type out the things I want to prove equal.21/02 02:29
copumpkinoh21/02 02:29
copumpkincan I make two separate 2-categories out of categories?21/02 02:58
copumpkinwith the two NT compositions I mentioned earlier?21/02 02:58
dolioWhich 2? Horizontal and vertical?21/02 03:00
copumpkinyeah21/02 03:08
copumpkinthe horizontal one seems kinda of weird21/02 03:08
dolioThen no, I don't think so. They both figure into a 2-category.21/02 03:08
dolioLet me see...21/02 03:09
dolioX, Y and Z are 0-cells.21/02 03:09
doliof1, f2 : X -> Y, g1, g2 : Y -> Z21/02 03:09
dolioI need more, don't I?21/02 03:10
doliof3 : X -> Y, g3 : Y -> Z21/02 03:10
copumpkinoh I see now21/02 03:10
copumpkinactually, no21/02 03:10
copumpkingo on :)21/02 03:11
doliot1 : f1 -> f2, t2 : f2 -> f3, u1 : g1 -> g2, u2 : g2 -> g321/02 03:11
copumpkin2-categories have a notion of horizontal and vertical composition, but in the 2-cat of cats it seems that vertical composition is functor composition (from what I can tell)21/02 03:11
dolioI'm going to have to write stuff down. Hold on.21/02 03:14
copumpkinncatlab is sort of clearing it up, but I should probably write this down too21/02 03:14
dolioAnyhow, Hom(X,Y) is a category, so t1 and t2 can be composed there.21/02 03:15
dolioIs that horizontal composition?21/02 03:16
doliou1 and u2 can of course also be composed for the same reason.21/02 03:16
dolioNo, that's vertical.21/02 03:17
copumpkinI see, I was just missing part of the definition of a 2-category21/02 03:17
copumpkin"The morphisms can be composed along the objects, while the 2-morphisms can be composed in two different directions: along objects – called vertical composition – and along morphisms – called horizontal composition. "21/02 03:18
dolioRight.21/02 03:18
copumpkinnext up, categories indexed by CoNat :)21/02 03:19
copumpkinjust kidding :P21/02 03:19
copumpkinwant to get the basic category stuff out of the way21/02 03:19
dolioI'd index by Nat.21/02 03:19
copumpkinbut what about omega categories!21/02 03:19
dolioInfinity categories have rather different problems.21/02 03:19
copumpkinjust think of all the lost expressiveness :(21/02 03:19
dolioFor instance, to some degree, you can define an (n+1)-category as a category enriched in an n-category.21/02 03:20
copumpkinso it actually feels like it wouldn't be too painful to define this with Nat and Fin21/02 03:20
dolioAnd that way, equivalences work out appropriately by induction.21/02 03:20
copumpkina 2-category has Fin (suc 2) -cells21/02 03:21
dolioHowever, that doesn't work for an infinity category.21/02 03:21
dolioWhich is why the people working on them come up with all the weird definitions.21/02 03:21
copumpkinokay, I'll not do that then :)21/02 03:21
dolioLike, "an infinity category is some sort of 'globular' or 'simplical' set....'21/02 03:22
* copumpkin runs away screaming21/02 03:22
dolioMe too.21/02 03:22
dolioAnyhow, I guess you get horizontal composition via _o_ for 1-cells.21/02 03:23
dolio_o_ needs to be a bifunctor, or something.21/02 03:24
dolioFrom Hom(X,Y) x Hom(Y,Z) to Hom(X,Z).21/02 03:24
dolioI don't know if that's sufficient.21/02 03:25
dolioThere's an interchange law as well.21/02 03:25
copumpkinany ideas about what universe level an n-category should live at? if I extend my current pattern, I'd need at least one level for 0-cells, then for everything above that, I'd need two levels for the cells and their equality21/02 03:26
copumpkinsounds like a nightmare21/02 03:26
dolioBut if you have a 2-cell from Hom(X,Y) and a 2-cell from Hom(Y,Z), the fact that composition is a functor gets you a 2-cell in Hom(X,Z).21/02 03:26
copumpkinI guess (Nat -> Level)21/02 03:26
dolioIt could live at any universe level.21/02 03:27
dolioJust like categories.21/02 03:27
copumpkinyeah, but I was wondering how best to represent which one it does live at21/02 03:27
copumpkinsuch that the cells aren't forced to live all at the same level21/02 03:28
dolioA 0-category (set) has a universe level.21/02 03:28
dolioA (suc n)-category has a collection of objects at universe i, and n-categories of arrows at level j, and thus lives at level (i \lub j).21/02 03:29
dolioBut that's pretty evil.21/02 03:29
copumpkinThe morphisms can be composed along the objects, while the 2-morphisms can be composed in two different directions: along objects – called vertical composition – and along morphisms – called horizontal composition.21/02 03:29
copumpkinwhoops21/02 03:29
copumpkinThe type of the constructor does not fit in the sort of the21/02 03:29
copumpkindatatype, since Setω is not less or equal than Set (_6 n F)21/02 03:29
copumpkin:(21/02 03:29
dolioBasically, an n-category takes a Vec Level (suc n), and lives at the lub of those levels.21/02 03:30
copumpkinyeah21/02 03:30
copumpkinbut I need a separate such Vec for equality levels21/02 03:30
copumpkinjust to be painfully general21/02 03:30
dolioI wouldn't be surprised if Agda isn't equipped for defining n-categories by induction.21/02 03:31
copumpkinit definitely didn't like record _-category (n : ℕ) (F : Fin (suc n) → Level)21/02 03:31
dolioThe question in the background is: can you forget about universe levels, and just have n-categories?21/02 03:31
copumpkinI can make it live in Set\_121/02 03:32
copumpkinand have    _-cell : (i : Fin (suc n)) → Set21/02 03:32
copumpkinI wouldn't be able to use my existing Category/Functor/NaturalTransformation machinery for it though21/02 03:33
copumpkinwell, I guess I could instantiate them all at level 021/02 03:33
dolioJust go --type-in-type!21/02 03:34
copumpkinlol21/02 03:34
copumpkinI think it'd be interesting to see how far this can be pushed21/02 03:34
dolioMaybe if you defined it the enriched way, a single interchange law between at the base level would be sufficient....21/02 03:35
dolioAnd interchange laws in whatever you're enriched in would combine to form whatever higher interchange laws are appropriate.21/02 03:36
dolioI'm going to assume that's the case. :)21/02 03:38
dolioCumulativity might be a significant benefit here.21/02 03:39
dolioThen you just pick a  'high enough' level to contain everything.21/02 03:39
dolioNo messing with lub.21/02 03:39
copumpkinyeah21/02 03:40
copumpkinthat'd be nice21/02 03:40
copumpkinokay, I'm going to put this down and get back to the safety of plain ol' 1-categories :P21/02 03:41
copumpkinmore exploration later :)21/02 03:41
copumpkinI kind of like the inductive idea21/02 03:41
copumpkinbut I can't really write inductive records21/02 03:41
dolioYeah.21/02 03:42
copumpkinI wonder if irrelevant modules are on the horizon21/02 03:42
dolioUltimately you'd end up with an n-nested sigma, or something close.21/02 03:42
dolio(n+1)-nested, maybe.21/02 03:42
copumpkinsince we now have irrelevance in a cabal version of agda, but none of the standard libraries seem to use it (because it breaks the nice re-exporting/flattening of algebraic structures)21/02 03:43
dolioWhich, Saizan gained a massive performance benefit for switching from nested sigmas to a record a day or two ago.21/02 03:43
copumpkinyeah, and I feel any way I approach it I'm still going to get a setomega21/02 03:43
copumpkinwell, maybe not21/02 03:43
copumpkinbut even with nested sigmas, I'm going to have something quantified over levels inside something else21/02 03:44
dolioMan, I always get thrown off by OPTIONS instead of LANGUAGE21/02 03:45
dolioI really need more memory.21/02 03:51
Saizanbtw, i'd like to come up with a minimal example of that nested sigmas performance problem, any suggestion for something i could write involving them that doesn't require many prerequisites?21/02 03:53
copumpkinSaizan: telescopey things?21/02 03:54
copumpkindolio: how much do you have?21/02 03:54
dolio2 gigs.21/02 03:54
copumpkinah21/02 03:55
copumpkinspeaking of nested sigmas21/02 03:55
copumpkinthat's how I implemented my arrow categories21/02 03:55
copumpkinso maybe that's why they're painful?21/02 03:55
dolioThat's how I did it, too.21/02 03:57
Saizancopumpkin: the last two functions here make a difference of ~40 seconds and ~800MB all by themselves: http://code.haskell.org/~Saizan/fooling/Check2.agda21/02 04:00
copumpkinwow21/02 04:00
copumpkinwell, I did notice that arrows were using 1.4GB total at the peak21/02 04:00
copumpkinand considering there wasn't much of interest in there, that seems like a likely culprit21/02 04:01
Saizanvector-like types defined by induction on the length don't seem to suffer from the same problem, btw21/02 04:03
doliohttp://hpaste.org/44191/ncategories_inductively21/02 04:04
copumpkinnice :)21/02 04:05
dolioIt gets pretty bad as soon as you want to put more than top there.21/02 04:05
copumpkindid you really use \lub as a function name?21/02 04:05
copumpkin:P21/02 04:05
dolio\Lub21/02 04:06
copumpkinyeah, I mean21/02 04:06
dolioBig lub.21/02 04:06
copumpkinthey look identical :P21/02 04:06
copumpkinnext up, o, O, and 0 as identifiers21/02 04:06
dolioThey don't in emacs, but my browser displays them pretty similarly.21/02 04:06
copumpkinthat's neat though21/02 04:07
Saizanyou should get better fonts, both of you :P21/02 04:07
copumpkinI'm always on the lookout for a nice monospaced font with lots of unicode :P21/02 04:07
copumpkinplease advise :)21/02 04:08
dolioEmacs somehow does it way better than anything else, here.21/02 04:08
dolioI think it pulls in symbols from several different fonts somehow.21/02 04:08
copumpkinOS renderers often do that21/02 04:09
copumpkinnot really sure what the rules are21/02 04:09
copumpkinsometimes I get empty boxes with some fonts, others I get symbols from a different font21/02 04:09
copumpkinmaybe some fonts pretend to support a character and in fact don't?21/02 04:09
* Saizan doesn't even know which fonts he's using21/02 04:24
copumpkinI really like that equational reasoning machinery21/02 04:51
copumpkinit makes things so much more pleasant21/02 04:51
copumpkinand is so simple21/02 04:51
Saizanyep, i just dislike having to duplicate the structure of the terms i'm proving equal in the proofs if i need any cong-like lemma21/02 04:54
copumpkinthere is a lot of unnecessary duplication but I actually like it because it shows a reader how things are being transformed21/02 04:54
copumpkinI used to do similar things with big chains of rewrites21/02 04:54
copumpkinbut that doesn't have the same benefit21/02 04:55
Saizanthe congs are more noise than clarification though, usually you just visually diff the two adjacent terms to see which subterm got transformed21/02 04:57
copumpkinyeah, fair enough21/02 04:57
copumpkinI don't actually get to use cong in mine though21/02 04:57
copumpkinand with the restricted form of cong I do get, I don't have to repeat the terms21/02 04:57
copumpkindoes this seem reasonable? http://snapplr.com/q98c21/02 05:11
copumpkinfor a functor21/02 05:11
dolioYes.21/02 05:12
copumpkinokay good21/02 05:14
RichardOHow would one define the binary naturals?21/02 05:14
copumpkinRichardO: boundedly?21/02 05:14
copumpkinthe agda standard library has an unbounded version of them21/02 05:14
RichardOunbounded21/02 05:14
copumpkinwhereas glguy and I made a bounded version21/02 05:14
copumpkinhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Bin.html#121/02 05:15
copumpkindolio: can you think of anywhere but functors and categories I need to think about preserving equality?21/02 05:15
RichardOAh, so they reverse the digits?21/02 05:16
copumpkinI only remembered to add it to functors when I tried to build stuff with them and was unable to :)21/02 05:16
dolioNot off the top of my head.21/02 05:16
dolioI mean, a setoid morphism is one that respects equality. So any time you have one of those.21/02 05:18
copumpkinyeah21/02 05:19
copumpkinI'd like to see a simple proof that http://www.cse.chalmers.se/~nad/listings/lib/Data.Bin.html#8190 is actually linear21/02 05:19
copumpkinhmm21/02 07:22
copumpkinwhat does equality on functors mean?21/02 07:22
dolioWhat do _you_ mean?21/02 07:24
copumpkin:P21/02 07:24
copumpkinwell, at first I was tempted to write that the two functors map objects to the same objects and morphisms to the same morphisms21/02 07:24
copumpkinbut considering I don't get object equality in my framework, and morphism equality seems to be sufficient21/02 07:25
copumpkinit seems sufficient to say that forall morphisms f, F f == G f21/02 07:25
dolioAre your equalities heterogeneous?21/02 07:26
copumpkinnope21/02 07:27
dolioAnyhow, the serious categorical answer is that 'equality' of functors is evil. You should only talk about (natural) isomorphism of functors.21/02 07:27
copumpkinI see21/02 07:27
dolioIf your equivalence isn't heterogeneous, it's hard for me to see how F f == G f could work.21/02 07:28
copumpkinyeah, it doesn't :P21/02 07:28
copumpkinalright, so _==_ = NaturalIsomorphism ?21/02 07:28
copumpkinthat seems clean21/02 07:28
copumpkinof course, that means I get a nice cyclic module dependency21/02 07:29
copumpkinnow I start to see why NAD made all those .Core modules :)21/02 07:29
dolioThis is why the collection of categories is a 2-category.21/02 07:32
copumpkingoes to show how profound my understanding of 2-categories was :)21/02 07:32
dolioFunctors are considered up to natural isomorphism, and categories are considered up to functors that are inverses up to natural isomorphism.21/02 07:32
copumpkin"arrows between, arrows, yo"21/02 07:32
copumpkinah21/02 07:32
dolioAnd natural transformations can be considered up to equality, I guess.21/02 07:33
copumpkinequality with respect to the "equality" on the functors?21/02 07:34
dolioYou're going to make me think about what it means? :)21/02 07:35
copumpkinlol21/02 07:35
copumpkinnope!21/02 07:35
dolioLet's see, C and D are categories, F, G : C -> D, phi, psi : F -> G...21/02 07:36
doliophi and psi are families of functions indexed by C-objects.21/02 07:37
dolioEr, families of morphisms.21/02 07:38
dolioSo phi = psi if phi_X = psi_X for all X.21/02 07:38
dolioFor morphism equality in D.21/02 07:38
copumpkinhm21/02 07:41
copumpkinfair enough21/02 07:41
copumpkinI'll implement that one in a bit21/02 07:41
copumpkinwant to prove that functor composition is associative with a unit first21/02 07:42
copumpkin"up to unique isomorphism"?21/02 07:42
* copumpkin will do the basics first :)21/02 07:43
dolioI mean, the truth is that this is usually built in some kind of set theory.21/02 07:43
dolioOr type theory.21/02 07:44
dolioSo there's an ambient equality you can appeal to.21/02 07:44
dolioAnd you can talk about equality of functors, and for composition and identity, they're equal on the nose.21/02 07:44
dolioOr, presumably. With enough proof irrelevance for the particulars of type theory.21/02 07:45
copumpkinseems kinda like a copout somehow :)21/02 07:46
dolioAnd you can talk about equality of objects that way.21/02 07:46
dolioIf you want to be fancy, you can have a setoid of objects.21/02 07:46
copumpkinI really wanted to avoid that though21/02 07:46
dolioRight.21/02 07:47
dolioAnd ignoring the built-in equality, and taking an equivalence for arrows is kind of in line with the categorical project.21/02 07:48
copumpkinGoal: _221 (_222 _223 _223) _22321/02 07:52
copumpkinman, proving natural isomorphism is an equivalence relation is rather scary21/02 07:56
dolioShouldn't be that bad, should it?21/02 07:58
copumpkinyeah, it looked scarier than it's turning out to be21/02 07:58
dolioWhy are you proving it's an equivalence relation, incidentally?21/02 08:08
copumpkinI need that to build (1-)category of categories21/02 08:08
dolioAh.21/02 08:08
dolioThat's a little weird, then.21/02 08:08
copumpkinI'm not used to thinking of such a thing as an equivalence relation21/02 08:08
dolioIt's like having a category where the objects are categories, and the morphisms are equivalence classes of functors.21/02 08:09
copumpkinhow else would you do it?21/02 08:09
dolioThe quotient of the set of functors by isomorphism.21/02 08:10
copumpkinand how would I encode that? :O21/02 08:10
dolioNormally it'd the 'category of categories' would have functors up to equality using the ambient set theory.21/02 08:10
dolioOr be a 2-category.21/02 08:10
dolioThe quotient thing is what you're doing.21/02 08:11
copumpkinoh okay21/02 08:11
copumpkinI'd still run into the same issue with a 2-category on equivalence of 1-cells wouldn't I?21/02 08:11
dolioA 2-category would be like...21/02 08:12
doliorecord 2-category where { 0-cell : Set ; 1-cell : Obj -> Obj -> Set ; 2-cell : {X Y : Obj} -> 1-cell X Y -> 1-cell X Y -> Setoid ; ... }21/02 08:13
dolioUsing your current methodology.21/02 08:13
dolioThen you define equivalence (isomorphism) of 1-cells by referring to the 2-cells.21/02 08:13
dolioAnd equivalence of 0-cells by referring to the 1-cells.21/02 08:13
copumpkinhmm!21/02 08:14
copumpkinand how are the 2-cells equivalent?21/02 08:14
dolioBy reference to the setoid. They're supposed to have equality defined for them.21/02 08:14
copumpkinoh okay, I see21/02 08:14
copumpkinso is this natural isomorphism is an equivalence relation thing taking me down the wrong path?21/02 08:15
dolioIt's the same currently for your setup. You take equality for morphisms, but nothing for objects.21/02 08:15
copumpkinyeah21/02 08:15
dolioHowever, given that setup, you can define isomorphism of objects.21/02 08:15
copumpkinyeah, I never did that21/02 08:15
copumpkinbut I guess I could21/02 08:15
copumpkinso wait, most of the talk of categories I've seen talks about equality and equivalence and isomorphism and so on, quite liberally21/02 08:16
copumpkinand says that a bicategory and a 2-category are distinguished by how strict the quality on 2-cells is21/02 08:16
copumpkinbut it all seems a bit hand-wavey21/02 08:17
copumpkin*equality21/02 08:17
dolioWell, okay, so there's two, at least, types of 2-categories.21/02 08:18
dolioStrict and weak.21/02 08:18
dolioBicategories are weak 2-categories, I think.21/02 08:19
dolioStrict categories have notions of equality where weak ones don't.21/02 08:20
copumpkinhmm!21/02 08:20
dolioSo, like, id . f = f, for a strict 2-category would be an equality on 1-cells.21/02 08:21
dolioIn a weak 2-category, it'd hold only up to isomorphism.21/02 08:21
copumpkinbut isomorphism is talking about equality on a different level21/02 08:21
dolioIn a weak 2-category, for any 1-cell f, there is an invertable 2-cell between id . f and f.21/02 08:23
dolioInvertible up to equality. Because 2-cells are considered up to equality.21/02 08:24
copumpkinyeah, but isn't talking about 1-cell up to ismorphism reducing it to equality between 2-cells?21/02 08:24
copumpkinyeah21/02 08:24
copumpkinokay21/02 08:24
dolioIn a strict 2-category, 1-cells are, too. So you might have two 1-cells that aren't equal, but are isomorphic.21/02 08:24
copumpkinso a strict 2-category has explicit equality for 1-cells too?21/02 08:24
dolioThat makes some problems go away, too.21/02 08:24
dolioLike with strict omega categories.21/02 08:25
dolioYou can say id . f = f as an equality, for any level of n-cells.21/02 08:25
copumpkinhm21/02 08:25
dolioFor a weak omega/infinity category, you want to say id . f is equivalent to f where equivalence is up to equivalent cells of the next higher level.21/02 08:26
dolioBut that's not well founded.21/02 08:26
dolioWhich is why you get the problems defining it I mentioned earlier.21/02 08:26
copumpkinhm21/02 08:27
copumpkin(it's amusing that naming a variable in a type that doesn't explicitly mention it can affect typechecking)21/02 08:28
copumpkinif I write AType -> _ vs. (x : AType) -> _21/02 08:28
dolioYeah.21/02 08:29
copumpkinsorry if I sound ADD and switch around a lot21/02 08:29
copumpkinaddicted to getting this thing working while talking :P21/02 08:30
dolioAlso \(x : A) -> e is different than \x -> e in ways other than that the former is easier to infer.21/02 08:30
copumpkinthis natural isomorphism transitivity thing is getting tricky21/02 08:35
dolioIt should be composition.21/02 08:40
copumpkinyeah, that part is the easy part21/02 08:40
copumpkinshowing that the composition is an isomorphism is a bit trickier21/02 08:40
copumpkinunless I'm just overcomplicating things21/02 08:41
dolioWhat's your definition of isomorphism?21/02 08:41
copumpkinf . g = id, and g . f = id21/02 08:41
copumpkinI just need to align the middles21/02 08:41
copumpkinand cancel them, then cancel the outsides21/02 08:41
dolioRight.21/02 08:42
copumpkinbut it gets a bit icky21/02 08:42
copumpkinthis won't do: http://snapplr.com/6wxq21/02 09:01
copumpkingotta rename my stuff :P21/02 09:01
Saizansigh, we should get around to fixing that stuff21/02 09:03
copumpkinokay, I haz equivalenz relashun21/02 09:22
copumpkinrather scary-looking in parts, but pretty straightforward21/02 09:23
* copumpkin now has a setoid of natural isomorphisms!21/02 09:30
copumpkinthis all feels rather meta21/02 09:31
copumpkinbut now I can do my equational reasoning for my functor associativity proof :P21/02 09:31
copumpkin</yakshave>21/02 09:31
copumpkinman, I'm really addicted to this stuff21/02 15:24
copumpkinI woke up way too early for how late I went to bed, and instead of going back to sleep I started poking at agda again21/02 15:25
copumpkinhmm, I have an uneasy feeling about my functor composition associativity proof21/02 16:22
copumpkinit seems too easy21/02 16:40
copumpkinsame with identity21/02 16:41
copumpkinwow, adding some definitional equality to this made my typechecking ridiculously slow21/02 17:35
doliocopumpkin: Since identity and associativity of functor composition 'really are' equal, it should be easy to show them isomorphic.21/02 17:36
copumpkinyeah, but it was terrifyingly easy :P21/02 17:36
copumpkinalso, xplat and rwbarton on #haskell seemed to think that natural isomorphism for functor equality was odd in the context of building a category of them21/02 17:37
copumpkinas did you :P21/02 17:37
copumpkinso now I'm working with the other approach21/02 17:37
dolioIt's odd for building a category, yes.21/02 17:40
copumpkinI'll keep around the natural isomorphism equivalence relation and the associativity code lives on in the git history21/02 17:40
copumpkinfind the missing hole! http://snapplr.com/mw9e21/02 17:41
copumpkinnote that ?2 has the wrong context for its location :P21/02 17:41
copumpkinholes in types seem generally buggy21/02 17:42
dolioIt might be due to some internal desugaring.21/02 17:43
dolioDefinitions inside records don't stay that way.21/02 17:43
copumpkinwhoa21/02 17:43
copumpkinyeah21/02 17:43
copumpkingot another weird error21/02 17:43
copumpkinever get "not a valid let declaration" with rewrite?21/02 17:44
copumpkinit's showing me a desugaring in the error21/02 17:45
copumpkinhttp://snapplr.com/s5eq21/02 17:45
dolioOkay, yeah. Definitions in a record prior to a field are desugared into lets.21/02 17:53
dolioAnd definitions in lets don't have the same power as general definitions.21/02 17:54
copumpkinick21/02 17:54
dolioYou can't do pattern matching, and presumably you can't do with and rewrite.21/02 17:54
copumpkinthis is all messed up21/02 17:54
dolioIt's strictly for naming expressions.21/02 17:54
copumpkinno, I mean, it's getting the holes all backwards and not letting me fill in things that are well typed21/02 17:54
dolioSomeone else was having weird issues with holes the other day...21/02 17:56
copumpkinI was having weird issues with holes the other day21/02 17:56
copumpkinbut these are even weirder21/02 17:56
dolioAh.21/02 17:57
copumpkinthe order's actually messed up too21/02 17:57
copumpkinf { }0 { }3 { }121/02 17:57
copumpkinmissing 2, and the ?0 and ?1 are the first and second arguments of f21/02 17:57
copumpkin3 is completely unrelated21/02 17:57
copumpkinhttp://snapplr.com/fw3n21/02 18:00
copumpkingah21/02 18:00
copumpkinI think having unsolved metas in universe levels messes it up21/02 18:01
copumpkinwow, typechecking on this file is just utterly fucked21/02 18:06
copumpkinnot just holewise21/02 18:06
copumpkinokay, getting somewhere21/02 19:19
copumpkinI have to "prove" the type of my functor equality axiom, but now that's out of the way, I think I'm good21/02 19:20
copumpkinhow can I prevent re-export of modules I define inside a record/module?21/02 19:25
dolioprivate21/02 19:28
copumpkinthanks21/02 19:31
copumpkinI'm starting to think it might be easier to just settle for heterogeneous equality in my basic category definition21/02 19:31
copumpkindo you think that'll be painful later on?21/02 19:31
copumpkinhaving a goal type with a proof in it is tiresome21/02 19:32
dolioI'm not sure how to do that.21/02 19:35
dolioHeterogeneous equivalence, that is.21/02 19:35
dolioThe reason you can give, say, extensional equality when the arrows are functions is that you know they're functions.21/02 19:37
copumpkinhm, yeah21/02 19:37
copumpkinthere must be a nice solution hiding somewhere here :P21/02 19:38
* ski idly wonders how common it would be to do stuff like `(P : |N -> Set) -> (n : |N) -> (n == Z -> P n) -> ((m : |N) -> n == S m -> P m -> P n) -> P n'21/02 20:29
skiinstead of `(P : |N -> Set) -> P Z -> ((m : |N) -> P m -> P (S m)) -> (n : |N) -> P n', i mean21/02 20:29
ski(similarly for other case/cata constructions, like for `Either A B'/`A + B', e.g.)21/02 20:29
copumpkinwhat would be the advantage?21/02 20:29
skithe former corresponds more to some phrasings of induction, "in the wild"21/02 20:30
skiit might also be that in the former, the type system will know that the scrutinee is equal to the respective pattern, in the relevant branch21/02 20:30
ski(instead of one having to prove that manually)21/02 20:31
ski.. but here i'm speculating a bit21/02 20:31
ski(iirc Coq has some kind of construction in their `match', which might be related to this)21/02 20:31
* npouillard reading http://www.cse.chalmers.se/~nad/listings/equality/README.html21/02 20:32
djahandarieWow, there sure is a lot of chat in here. :P21/02 21:23
djahandarie04:17 < copumpkin> if I write AType -> _ vs. (x : AType) -> _21/02 21:23
djahandarieHow does this affect typechecking?21/02 21:23
djahandarie(If you don't even do anything with x later)21/02 21:23
copumpkinif it infers _ to need to refer to that AType21/02 21:23
copumpkinit won't be able to unless it's named21/02 21:24
djahandarieAh, I see.21/02 21:24
djahandarieCould that somehow arise when using foralls also?21/02 21:24
copumpkindon't think so21/02 21:25
copumpkinforalls are only names21/02 21:25
copumpkinbut if it can't infer the type or the type refers to other variables21/02 21:25
copumpkinthen it'll turn yellow21/02 21:25
copumpkinthis latest proof quantifies over not one, not two21/02 23:04
copumpkinbut eighteen universe levels21/02 23:04
copumpkin:(21/02 23:04
copumpkinoh maybe just 9 of them21/02 23:05
Saizanthere should probably be an award for the most universe polymorphic definition21/02 23:06
copumpkinI misunderestimated! it's actually 12 universe levels :P21/02 23:07
copumpkin3 for each category21/02 23:07
copumpkinI have 12 universe levels, 4 categories, 6 functors, and three natural transformations21/02 23:07
* copumpkin feels accomplished21/02 23:08
--- Day changed Tue Feb 22 2011
copumpkinman, I love finding that a big scary-looking proof is fairly easy22/02 00:27
* copumpkin wonders whether the interchange law will quantify over even more universes!22/02 00:30
copumpkinprobably not though22/02 00:30
copumpkinwelcome to the silence22/02 05:41
kmcthe words of the prophets are written on the subway walls22/02 05:41
kmchi copumpkin22/02 05:41
copumpkinhi!22/02 05:42
copumpkin:)22/02 05:43
djahandarieHi kmc22/02 05:46
kmchi djahandarie22/02 05:58
kmccool kids only itt22/02 05:58
copumpkinitt technical institute?22/02 05:59
kmcin this thread22/02 05:59
kmcbut, yes22/02 05:59
freiksenetciting from a code generation in agda "generate it with agda. Sometimes you can mindlessly bash the keyboard there, type checking will still guarantee correctness"22/02 09:31
freiksenetfrom a code generation discussion*22/02 09:31
liyangfreiksenet: in other words, you can write Agda while drunk. (Credits to Dr Altenkirch.)22/02 14:22
freiksenetliyang: hah22/02 14:23
freiksenetyeah, that's an even more beautifully formed description of agda :D22/02 14:24
dolioI've written C++ while drunk.22/02 14:26
dolioWasn't that hard.22/02 14:26
copumpkinwas it correct though?22/02 14:26
dolioOf course.22/02 14:26
liyangBallmer peak?22/02 14:27
dolioIt was, like, some freshman programming assignment, though.22/02 14:27
dolioSo I suppose it couldn't have been that hard in the first place.22/02 14:28
dolioI wouldn't recommend trying to write Boost-level templates, for instance.22/02 14:30
djahandarieI don't think I could write C++ sober22/02 15:02
freiksenetI wouldn't recomenned trying to write boost-level templates even sober :|22/02 15:03
Adamantnot writing C++ sober is kinda like doing chainsaw juggling under the influence. yes, it helps take away the pain and fear, but I'm not sure that's a good thing for the end result.22/02 15:05
freiksenetI would say writing C++ is a bad thing for the end result.22/02 15:07
Adamanttrue, but so is chainsaw juggling22/02 15:07
doliocopumpkin: So, are you up to more than 12 levels yet?22/02 16:56
copumpkinno :(22/02 16:56
copumpkinI was hoping the interchange law would take more22/02 16:56
copumpkinbut it only used 922/02 16:56
dolioYeah. Only 3 categories involved.22/02 16:56
copumpkincan you think of any constructions that involve more than 4 categories?22/02 16:56
dolioNot off the top of my head.22/02 16:58
dolioKan extensions are 3.22/02 16:59
copumpkindamn22/02 16:59
copumpkinI'll need to devise some new and crazy constructions to exercise my agda-fu22/02 16:59
dolioMaybe if you defined pullbacks of categories or something.22/02 17:00
copumpkinoh that could work!22/02 17:00
copumpkinseems like I could get up to five there22/02 17:00
dolioThat involves 5, maybe.22/02 17:00
dolioYeah.22/02 17:00
copumpkinmmm, good idea22/02 17:00
djahandarieHaven't you broken Agda yet copumpkin? :P22/02 17:00
copumpkinbut I guess I need a category of categories first22/02 17:00
copumpkinand for that I need to resolve this functor stuff22/02 17:00
copumpkindjahandarie: I think anyone using agda for anything nontrivial breaks agda once every few hours :)22/02 17:01
dolioWell, you don't _need_ that. You can just define an operation that would be a pullback in the category of categories.22/02 17:01
dolioOr the 2-category of categories.22/02 17:01
copumpkinyeah, fair enough22/02 17:01
copumpkinI should also dust off my old comma category code and move it to the new framework22/02 17:12
copumpkinman, upenn's internet connection sucks :P22/02 17:42
byorgeycopumpkin: wait, you are at penn?22/02 18:23
copumpkinnope22/02 18:23
copumpkinI was remarking on ccasin's connection issues :)22/02 18:24
byorgeyoh, haha22/02 18:24
byorgeyour internet connection is usually quite good actually, I don't know why he is having problems22/02 18:25
copumpkinyeah, I'd imagine a big university would have a decent connection :)22/02 18:26
copumpkinhe's back!22/02 18:27
ccasinsorry, were my join/part messages annoying?22/02 18:28
copumpkindidn't bother me :)22/02 18:28
ccasintrying to get the damn irssi config right :)22/02 18:28
xplati've looked at the homepage but i'm having trouble figuring out where to get agda-mode22/02 20:33
copumpkinit's built in22/02 20:35
copumpkinonce you've cabal-installed agda22/02 20:35
copumpkinjust type agda-mode in your shell22/02 20:35
copumpkinagda-mode setup22/02 20:35
xplatis emacs23 good enough to run it?22/02 20:36
xplat(fsf)22/02 20:36
copumpkinI think so22/02 20:36
copumpkinI use aquamacs but I don't think it cares what emacs you have22/02 20:36
xplati know real unicode support is a pretty new thing to emacsen22/02 20:36
copumpkinah, not sure then22/02 20:36
copumpkinI'm not a regular emacs user22/02 20:36
copumpkinI only use it for agda22/02 20:37
dantenIm using 23.2.1 and it works for me22/02 20:37
xplatdanten: excellent, thanks22/02 20:37
danten:)22/02 20:38
copumpkinxplat: have you done any DT stuff before?22/02 20:38
xplatcopumpkin: theory, not so much practice22/02 20:41
copumpkinI see22/02 20:42
xplat(and yeah, i know even the practice is mostly theory :))22/02 20:42
copumpkinthe interactivity is fun22/02 20:42
copumpkinI'd start with some simple proofs to figure out the tools22/02 20:42
copumpkinas waiting 2 minutes to typecheck simple changes might not be very fun at first22/02 20:42
xplateep! :)22/02 20:43
copumpkinluckily, I've never experienced waits as long as the ones dolio's described22/02 20:43
copumpkinalthough I fear for those monoidal categories22/02 20:43
copumpkinalso, if you can think of a more meaningful module layout, I'd be happy to take it22/02 20:44
copumpkinmy goal is to have simple concrete definitions be the basic ones, then provide equivalences with fancier things22/02 20:44
copumpkinso e.g., a fairly simple direct definition of a monad as a functor with a couple of NTs, then separately proving that it's the composition of adjoint functors or a monoid object in cat of endofunctors22/02 20:45
xplatwait until you have to define anafunctors so you can work with anafunctors of limits when you don't have the axiom of choice ...22/02 20:46
* copumpkin doesn't even know what an anafunctor is! :P22/02 20:46
xplati still have trouble dealing with anafunctors on paper :þ22/02 20:46
copumpkinone thing I'd really like to do22/02 20:47
copumpkinis a graph of CT concepts22/02 20:47
copumpkinwith edges representing "is an instance of" and other relationships22/02 20:47
xplatthe closest thing to that i've seen is the CT wiki, but it's of course tough to get an overview22/02 20:47
copumpkinyou mean ncatlab?22/02 20:48
xplatyeah22/02 20:48
copumpkinyeah, that's got loads of good stuff22/02 20:48
copumpkinbut it's also got loads of stuff I've never heard of and probably never will22/02 20:48
copumpkindon't want to go too crazy22/02 20:48
copumpkina bit like a typeclassopedia of CT concepts22/02 20:48
copumpkinfor high-level overview22/02 20:48
copumpkinanyway, that's mostly unrelated :)22/02 20:49
copumpkin(a category of CT concepts! :P)22/02 20:50
copumpkinwhich I guess would just be a subcategory of the category of relations22/02 20:50
xplatFile mode specification error: (file-error "Cannot open load file" "haskell-indent")22/02 20:56
copumpkinhmm!22/02 20:56
xplatdoes that need installed separately from somewhere?22/02 20:57
dantenyes, haskell-mode22/02 20:58
xplatwhere do i get that from?22/02 21:01
dantenhttp://www.haskell.org/haskellwiki/Haskell_mode_for_Emacs22/02 21:03
dantenit seems to have darcs repo for developement at least22/02 21:03
dantenIm using Archlinux and for me it was in Pacman as emacs-haskell-mode22/02 21:04
pumpkinI like the NPOV on ncatlab22/02 21:20
pumpkindoesn't the eckmann-hilton argument tell us that vertical and horizontal composition of NTs are the same operation, and it's commutative?22/02 21:23
pumpkinthat is clearly not true, but what's wrong?22/02 21:23
xplati'm sure when they get big enough, they'll have a huge reorg and cleanup that will drive away half the community just like tvtropes22/02 21:28
copumpkin:P22/02 21:28
copumpkinoh I see22/02 21:37
copumpkineckmann-hilton says that vertical and horizontal composition are the same when you have your domain NTs all over the same functor?22/02 21:38
copumpkin(and commutative)22/02 21:39
xplathow do i import == from the standard library?22/02 21:50
xplatcopumpkin: then it's saying that NTs from an endofunctor to itself commute?22/02 21:50
xplati could believe that22/02 21:50
doliopumpkin: 2-categories aren't monoids.22/02 22:15
pumpkinstill22/02 22:16
dolioIf you ensure that they only have one 0-cell, and one 1-cell, though, you get a commutative monoid, though.22/02 22:16
dolioIf I'm not mistaken.22/02 22:16
pumpkinyeah, I just mean I can apply my interchange proof to a pair of NTs and show that if the NTs are over a single functor, they commute22/02 22:16
pumpkinseems odd22/02 22:17
dolioThey don't commute in general because the types make no sense.22/02 22:17
pumpkinyeah22/02 22:17
pumpkinbut where possible, they do commute, and vertical and horizontal are the same?22/02 22:17
pumpkinon "endonaturaltransformations"? :P22/02 22:17
dolioPresumably.22/02 22:18
pumpkininteresting22/02 22:18
pumpkin> reverse . take 5 $ [1..10]22/02 22:20
lambdabot  [5,4,3,2,1]22/02 22:20
pumpkin> take 5 . reverse $ [1..10]22/02 22:20
lambdabot  [10,9,8,7,6]22/02 22:20
pumpkinI suppose it isn't talking about that22/02 22:21
dolioI don't know why it wouldn't be, so maybe I'm wrong.22/02 22:22
pumpkinit seems like a trivial conclusion from the interchange law, so I'm confused :)22/02 22:22
pumpkinxplat: any ideas?22/02 22:23
dolioWhat's horizontal composition look like?22/02 22:24
dolioWait...22/02 22:24
dolioDoesn't horizontal composition of F -> F and G -> G give FG -> FG?22/02 22:24
dolioYes.22/02 22:27
xplater, yeah, then you'd need it to be an idempotent functor22/02 22:27
pumpkinyeah22/02 22:28
pumpkinhmm22/02 22:28
dolioRight.22/02 22:28
pumpkinusing interchange I only ever get id on one side though22/02 22:28
pumpkinstill confused22/02 22:28
pumpkinif this module took less time to typecheck I'd play with it22/02 22:28
pumpkinneed to split it out into a separate file22/02 22:28
pumpkinit'll be my first time using setoid reasoning on natural transformations22/02 22:28
xplati'm still getting read timeouts accessing the agda wiki22/02 22:29
xplatcan you tell me how to import definitional equality from the standard library?22/02 22:29
xplat(for the simple set of proofs about peano naturals i'm playing with)22/02 22:30
* xplat sighs22/02 22:34
xplati suppose i'll have to just write my own22/02 22:35
kulakowskipumpkin: The case that you were talking about above, with just one object and one morphism, then Eckmann-Hilton holds for horizontal/vertical composition. http://ncatlab.org/nlab/show/Eckmann-Hilton+argument22/02 22:35
xplatsucc-eq m n eq = (subst {Peano} {λ (x : Peano) -> succ m == succ x } m n eq (refl (succ m)))22/02 23:10
xplathow much of that can i trim down?22/02 23:13
copumpkinremove parens, remove implicit argument22/02 23:14
copumpkinmake refl not mention its argument22/02 23:14
copumpkinquite a bit :)22/02 23:14
copumpkinin fact, just write cong22/02 23:14
copumpkinand then talk about cong succ22/02 23:14
--- Day changed Wed Feb 23 2011
copumpkinwtf23/02 03:04
copumpkinhttp://hpaste.org/44225/quite_a_few_unsolved_metas23/02 03:10
dolioHow did you even get all that?23/02 03:12
copumpkinthis little thing23/02 03:14
copumpkinhttp://snapplr.com/q4t423/02 03:14
dolioNo, I mean all 300 lines. Emacs never displays more than like 10 lines in the bottom here.23/02 03:15
copumpkinoh it does for me23/02 03:15
copumpkinnot sure23/02 03:15
dolioMaybe it scrolls, I don't know.23/02 03:15
copumpkinit feels like it should be able to figure out all those metas from the other stuff I gave it23/02 03:17
dolioThe yellow on equiv is a bad sign, I think.23/02 03:19
dolioI wouldn't be surprised if fixing that helped quite a bit.23/02 03:19
copumpkinyeah, it's usually yellow until I use sym23/02 03:19
copumpkinoh I see what's wrong23/02 03:35
copumpkinbut am too lazy to fix it right now23/02 03:36
copumpkinhttp://coq.inria.fr/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html23/02 04:09
copumpkindoes anyone see how that Equal_hom works?23/02 04:10
copumpkinlooks sort of like JM equality over an arbitrary setoid, sort of like what I was talking about before23/02 04:25
* copumpkin plays with the same approach23/02 04:26
copumpkinwtf23/02 04:38
copumpkinsometimes agda makes no sense to me23/02 04:40
copumpkinso I have23/02 04:40
copumpkindata _∼_ {o ℓ e} {C : Category o ℓ e} {A B} (f : Category.Hom C A B) : ∀ {X Y} → Category.Hom C X Y → Set (ℓ ⊔ e) where23/02 04:40
copumpkin  refl : {g : Category.Hom C A B} → Category._≡_ C f g → _∼_ {C = C} f g23/02 04:40
copumpkinnotice the implicit application in the return value of refl23/02 04:41
copumpkinwithout it, I get yellow23/02 04:41
copumpkinit's on the left!!23/02 04:41
copumpkinhow can it not figure that out?23/02 04:41
copumpkinit's really bad at inferring stuff on this type23/02 04:58
copumpkinand the fucking w' variable comes back to bite me23/02 05:08
copumpkinbut if I can get this type working well, it seems like it's the right way to do functor equality23/02 05:14
copumpkindjahandarie: hey hey, moar video23/02 05:19
copumpkinhttp://www.youtube.com/view_play_list?p=44F162A8B8CB7C8723/02 05:19
dolioOh, right. The datatype is heterogeneous but the constructor is homogeneous.23/02 05:20
copumpkinhave any idea why agda can't figure out the constructor on it?23/02 05:20
copumpkinam I missing some reason why that'd be hard?23/02 05:21
dolioConsidering it's a parameter, and not an index, no.23/02 05:22
copumpkinthat's why I was surprised23/02 05:23
copumpkinyet without it the ~ turns yellow23/02 05:23
copumpkinone issue with this type is that its constructor seems remarkably difficult to match on23/02 05:41
copumpkinin fact, I have yet to succeed23/02 05:41
copumpkinwow, voevodsky is on github now :P23/02 05:48
greapHey. I'm just trying to get the emacs mode working, and I get the error: File mode specification error: (file-error "Cannot open load file" "haskell-ghci")23/02 07:18
greapDoes anyone know what to do with this?23/02 07:18
kavabeanHi does anyone know how to put an upper case character reduced in size next to an \entails?  I'd like to write this  ⊢v in an agda def.23/02 12:41
xplatwhat is wrong with this definition?23/02 16:49
xplat_==>_by_ : ∀ {A : Set} {x y : A} -> (x == y) (z : A) (y == z) -> (x == z)23/02 16:50
xplatrefl ==> _ by refl = refl23/02 16:50
xplatit gets a parse error starting at the A in (z : A)23/02 16:51
danteneither you need a -> or you give a name to x == y23/02 16:52
danten(x == y) -> (z : A) -> (y == z) or (p1 : x == y)(z : A)(p2 : y == z)23/02 16:52
xplatah, thanks, i used the version with loads of arrows and got it compiling23/02 16:54
xplathopefully this function will make my equality proofs much easier to write and read23/02 16:54
dantenhave you looked at equality reasoning?23/02 16:55
xplatno; not sure where to go to look at it23/02 16:55
dantenhttp://www.cse.chalmers.se/~nad/listings/lib/Data.Nat.Properties.html there is example how to use it23/02 16:56
dantenfor example +-comm23/02 16:56
xplathm, that is nice ... very much the equational style i was aiming for.  it's called _≡(_)_?23/02 17:01
pumpkinwhich?23/02 17:01
pumpkinoh, there's PreorderReasoning23/02 17:02
pumpkinand SetoidReasoning, which is a renaming of it23/02 17:02
pumpkinso if you have a setoid or a preorder, you can use it23/02 17:02
pumpkinI stole it for my CT library too :)23/02 17:02
pumpkindolio: I worked through the eckmann-hilton argument a bit more by hand (agda was taking too long) and I think it basically reduces to saying that NTs over the identity functor can be composed commutatively in both ways, and that in that case the compositions are equal23/02 17:08
pumpkinso not a very groundbreaking discovery :)23/02 17:08
djahandariepumpkin, ah nice, thanks. I just happened to come across that on twitter. :P23/02 17:16
pumpkinfrom me? :P23/02 17:16
djahandarieNope, jamesiry23/02 17:17
djahandarieI see that you have tweeted it also :P23/02 17:18
pumpkinlol23/02 17:18
djahandarie11hrs is way too far back though because the Japanese people I follow tweet at the speed of light23/02 17:18
pumpkinI'm guessing he must've seen it from me, since I'm not sure where else he'd have come across it!23/02 17:18
pumpkinyet he didn't retweet :(23/02 17:18
djahandarie:(23/02 17:18
* pumpkin is a twitter whore23/02 17:18
xplatcopumpkin: now that i've played around with equality proofs enough to understand the design space a little, i'm coming around to thinking arrows need heterogenous equality23/02 19:50
copumpkinI've decided they don't! :P23/02 19:51
copumpkinwhat makes you think so?23/02 19:51
xplatwell, maybe i'm still a couple of days behind you :)23/02 19:52
xplati understand why you wrote preserve₁ with the rather gnarly-looking type you did, and i remembered the first place i saw heterogenous equality, and finally understood why it was introduced, and it seems like the same kind of situation to me23/02 19:53
copumpkinwell, my current "solution" is to have a fake heterogeneous equality just for functors23/02 19:54
copumpkinyou can take a look at what's currently in the functor module in git23/02 19:54
copumpkinI borrowed the idea from a coq version I found23/02 19:54
copumpkinhowever, it's proving a real pain to use23/02 19:54
copumpkinbut I feel it's the right way to go about it23/02 19:54
copumpkinhttps://github.com/pumpkin/categories/blob/master/Category/Functor.agda23/02 19:55
copumpkinfirst of all, agda's doing something surprising on that [_]_~_ type23/02 19:55
copumpkinwhich is why it's got the explicit category parameter in it23/02 19:55
xplatbtw, how do subscripts work in agda?  are they just characters like any other?23/02 19:56
copumpkinyeah23/02 19:56
xplatit'd be nice to have subscripting built into a proof assistant somehow23/02 19:59
copumpkinyeah23/02 19:59
xplatmathml syntax?23/02 19:59
copumpkinI agree23/02 19:59
copumpkinnot sure about mathml23/02 19:59
copumpkinI want it to be machine-readable but fuck everything about xml23/02 19:59
xplatif mathml editors were good enough one could build the language syntax on top of mathml like is normally done with text23/02 20:00
copumpkinyeah23/02 20:00
xplatbut i don't know that mathml editors are actually there yet, or ever will be23/02 20:00
xplatmathml syntax would definitely be Wrong if your editor shows you the pointy brackets all the time23/02 20:01
copumpkinyeah :)23/02 20:01
xplatokay, so [_]_~_ is heterogenous equality, indexed by the host category for mysterious reasons23/02 20:07
copumpkinwell, not indexed by the host category23/02 20:10
copumpkinwhich makes it even more mysterious23/02 20:10
copumpkinthe category is on the left of the :23/02 20:10
copumpkinwhich makes it trivial for it to figure out23/02 20:10
copumpkinyet if I leave it implicit, it fails to infer it23/02 20:10
xplatah, hm, it does seem funny how it doesn't get it from the type of f23/02 20:13
xplatwhat is the . before equiv?23/02 20:13
copumpkinmakes it irrelevant23/02 20:13
copumpkinmeans it can be erased at compile time (and runtime)23/02 20:13
copumpkinand there's a dependency system for it23/02 20:14
xplatoh, this is the replacement for Prop23/02 20:14
copumpkinpretty much23/02 20:14
copumpkina bit more fine-grained, as far as I can tell23/02 20:14
xplatso the dependency system ensures that only things that are erased can depend on things that are erased23/02 20:15
copumpkinyeah23/02 20:16
xplatis there anything like sections for mixfix operators or do you always have to use function form/lambdas?23/02 20:17
copumpkinno sections yet23/02 20:18
copumpkinI think it's planned in the distant future23/02 20:18
copumpkinbut sounds like a nightmare23/02 20:19
xplatpresumably the blanks would have to be marked with — or something23/02 20:19
copumpkinyeah23/02 20:20
xplati have a hard enough time figuring out how that stuff can get parsed at all23/02 20:20
xplati mean, if you restricted sections to only simple infix operators maybe something could be done, but that doesn't seem in the spirit23/02 20:21
copumpkinyeah23/02 20:21
copumpkinI think the main driving force behind the mixfix (I may be wrong) is NAD, and I get the impression he's rather busy with other more pressing issues than syntax these days23/02 20:22
xplatthat would make three kinds of blanks -- _ for a blank to infer, ? for a blank to work around, and {something} for a blank to move out as a new argument23/02 20:22
copumpkinyeah :P23/02 20:23
copumpkinthen we start looking like scala23/02 20:23
xplatno, scala would use the _ for all three kinds :)23/02 20:23
copumpkin:P23/02 20:23
xplatyou can write entire programs in scala using nothing but _ and whitespace :)23/02 20:24
* copumpkin cringes23/02 20:24
xplatokay, actually you can't, but with how overloaded it is you ought to be able to23/02 20:24
doliocopumpkin: That would be the 2-category with trivial 0 and 1 cells, certainly.23/02 22:43
dolioIt'd be a little more interesting if it could work for any idempotent functor like xplat said. But I don't know how common those are.23/02 22:45
dolioMaybe identity is the only one.23/02 22:45
dolioThinking about it, it's difficult for me to imagine an idempotent functor that isn't identity.23/02 22:58
Mathnerd314so you need a * a = a? where a :: Functor and * is functor composition?23/02 22:59
dolioYes. I guess if you have, say, the natural numbers as a category...23/02 23:01
dolioYou can have a functor that takes 0 to 1, and everything else to itself.23/02 23:02
dolioThen you have FF0 = F1 = 1 = F023/02 23:02
dolioAnd FFn = Fn.23/02 23:02
dolioSo they can possibly exist.23/02 23:03
kulakowskidolio: Would vector space projections be an example of what you are talking about? An idempodent endofunctor?23/02 23:34
--- Day changed Thu Feb 24 2011
doliokulakowski: I don't know. It's been a long time since I did anything linear algebra related.24/02 00:35
dolioDo you mean taking a vector to its component along another vector? Then that sounds right.24/02 00:36
dolioAssuming that's a functor somehow.24/02 00:36
dolioThe functor would have to be idempotent in its action on morphisms, too, but that can probably be arranged.24/02 00:37
kulakowskiDolio: Make a category out of a vector space V24/02 00:37
kulakowskiobjects are subspaces, morphisms linear maps24/02 00:38
kulakowskiThen for any subspace W, you can make a functor that sends objects to the projections into W, and maps to the restrictions24/02 00:39
kulakowskiAlso you need an inner product on V for orthogonality24/02 00:39
dolioAnd if you take a space, project it on to W, and then project the result onto W again, you get the same thing as projecting once?24/02 00:40
dolioEr, into.24/02 00:40
kulakowskiYeah. That projections are idempotent is not too hard to prove, once you've played around with the inner product.24/02 00:41
dolioOkay. Then that sounds like it would work.24/02 00:41
kulakowskiYeah. I am sure there are other examples, and not contrived ones.24/02 00:45
dolioI tend to be in functors-as-type-constructors mode mentally, and it's hard to come up with examples there.24/02 00:45
dolioOr, harder.24/02 00:46
dolioOf course \_ -> X, for some type X is an example, if you can construct that.24/02 00:47
dolioThat probably counts as contrived, though.24/02 00:48
kulakowskidolio: I'll try and think of something more type-like.24/02 00:54
dolioThe thing is, in Haskell for instance, you can't really even do \_ -> X, first-class at least.24/02 00:54
dolioYou can do 'data K a b = K a', but then K a (K a b) isn't recognized as identical to K a b.24/02 00:55
Mathnerd314type families?24/02 01:08
dolioYes.24/02 01:08
dolioType families aren't first-class, though.24/02 01:08
dolioOf course, restricting yourself to first-class type constructs in Haskell is arbitrary.24/02 01:09
djahandarieIt would be interesting if they were first-class.24/02 01:09
Mathnerd314they're implemented in GHC... how first-class can you get?24/02 01:09
djahandarieMathnerd314, first-class enough to pass it as a value? :P24/02 01:09
dolioYou can't instantiate a variable of kind * -> * to a type family.24/02 01:09
dolioUnless I'm mistaken.24/02 01:10
Mathnerd314ah, ok. You can in Agda... ?24/02 01:10
dolioAgda has functions at the type level, yeah.24/02 01:10
dolioOf course, type families let you do case analysis on types, which you can't do in Agda.24/02 01:11
djahandarieWouldn't it be better to say "Agda's functions accept types as input"?24/02 01:11
djahandarieI guess that doesn't mean as much though24/02 01:11
copumpkinyou don't get eliminators on types24/02 01:11
dolioSure, I guess. There's no separate type level.24/02 01:11
Saizando defintions in mutual blocks behave strangely wrt reduction?24/02 01:20
dolioWhat's strangely mean?24/02 01:20
Saizanwell, i don't get why a call to some function defined in another mutual block doesn't reduce in my current goal24/02 01:23
dolioOh. Possibly, I guess.24/02 01:24
dolioThere are decent reasons for not having definitions within a given mutual block reduce, I think. Maybe it's overzealous in that regard.24/02 01:25
Saizansounds possible, even if C-c C-n behaves as i'd expect24/02 01:27
djahandariedolio^op you mean? :)24/02 01:50
dolioI don't have that one registered.24/02 01:50
* djahandarie is certain his nick would get beyond impossible to comprehend if he tried tacking on any of these hip things to it24/02 01:51
pumpkincodjahandarie24/02 01:51
djahandarieAt least maybe this way people wouldn't think I'm a DJ.24/02 01:51
pumpkinthey might think you're a fish though24/02 01:52
djahandarieI'm just a cod now.24/02 01:52
djahandarieHaha, yeah. :(24/02 01:52
djahandarieOr a codomain.24/02 01:52
pumpkinopdjahandarie24/02 01:52
pumpkinpdj isn't a string of letters you see very often24/02 01:52
djahandarieNow that is fairly incomprehensible.24/02 01:52
pumpkinso if you have a constructor that's very difficult to match on24/02 02:33
pumpkinand a with clause that would introduce the indices the expressions the constructor wants to play with causes the dreaded != w' error24/02 02:34
pumpkinwhat would you do?24/02 02:34
pumpkinwhat are strategies for matching difficult constructors?24/02 02:34
copumpkinman, I succeeded24/02 03:12
copumpkinwell, I got further, anyway24/02 03:13
copumpkinyay24/02 03:16
copumpkinthat was way too hard24/02 03:16
xplatwas the difficult constructor [_]≡_ ?24/02 03:21
copumpkinyeah, too dependent for a with block24/02 03:22
copumpkinso I had to do it manually24/02 03:22
xplatalso, any clue why i'm getting parse errors loading files with a lot of irrelevant definitions?24/02 03:22
copumpkinoh24/02 03:23
copumpkinnot when loading, but I get parse errors in unexpected places sometimes24/02 03:23
xplati seem to get them predictably when there's an irrelevance dot on a type signature at top or record level24/02 03:23
copumpkinokay, I have an equivalence relation on functors! :D24/02 03:24
* copumpkin cheers24/02 03:24
copumpkinxplat: weird, maybe worth submitting a bug24/02 03:24
djahandariecopumpkin, how do you do it manually?24/02 03:24
copumpkindjahandarie: write a very dependent helper function24/02 03:24
dolioLike very dependent types?24/02 03:25
dolioFor implementing dependent records?24/02 03:25
copumpkinfine, just sort of dependent types :)24/02 03:26
copumpkindependenter than with likes24/02 03:26
xplatiwbni you could generate equality proofs by just defining a few rewrite rules and feeding them to a (custom, if needed) equational theory solver24/02 03:27
xplatinstead of futzing around throwing oblique hints at the typechecker24/02 03:27
xplatit's like, i'm trying to prove a theorem here, not ask the compiler to the prom24/02 03:27
copumpkinlol24/02 03:28
copumpkinI feel like that sometimes24/02 03:28
greapHey guys :) I've finally got emacs running agda, how do I use the repl? I've just got Bool and not defined, I'd like to test not in the repl, but have no idea how to do this from emacs...24/02 03:46
copumpkinI wouldn't use the repl24/02 03:46
copumpkinin emacs, just do C-c C-n24/02 03:46
copumpkinand type in the expression you'd want to run in the repl24/02 03:46
greapAh awesome24/02 03:47
greapI've always used vim until now, so I'm completely lost :D24/02 03:47
greapWould that be worth adding to http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode, or is it just taken as basic knowledge?24/02 03:48
copumpkinhm, I thought it was somewhere, but sure24/02 03:48
greapOh that's listed as normalise...24/02 03:48
copumpkinyep24/02 03:49
copumpkinevaluate and normalize are more or less the same :)24/02 03:49
greapThanks a lot copumpkin. I believe you've helped me out in #haskell too :)24/02 03:49
copumpkinno problem24/02 04:06
copumpkingah, proofs are hard24/02 04:06
copumpkinlet's go shopping24/02 04:06
copumpkinhmm!24/02 05:14
copumpkinproving that functor composition respects this notion of equivalence is tricky24/02 05:15
copumpkinthat's all I'm missing before I can build myself the category of categories24/02 05:16
copumpkinor even the 2-category of categories (if I had such a structure)24/02 05:16
djahandarieIs it more elegant to define Cat as a 2-category with natural transformations as 2-morphisms, or a 2-category as a category enriched over Cat?24/02 05:18
dolioYou need to tweak the usual definition of "enriched" to make a 2-category a Cat-enriched category.24/02 05:20
dolioUnless you mean a strict 2-category.24/02 05:21
djahandarieAh, I see24/02 05:22
* djahandarie just read ncatlab24/02 05:22
copumpkinthis can't be right24/02 05:22
copumpkinI think agda gets confused sometimes :)24/02 05:22
djahandarie"Specifically, if we fix a meaning of ∞-category, however weak or strict we wish, then we can define a 2-category to be an ∞-category such that every 3-morphism is an equivalence, and all parallel pairs of j-morphisms are equivalent for j≥3." This sounds evil.24/02 05:24
dolioThat's I think, the leading way of defining n-categories.24/02 05:25
dolioAlthough I couldn't really tell you why.24/02 05:25
* djahandarie suddenly finds a bunch of articles on ncatlab that he has never seen before24/02 05:26
djahandarieI could spend all day browsing this thing and learning useless terms24/02 05:26
dolioYeah.24/02 05:26
djahandariePerhaps it would be a better investment to sleep instead.24/02 05:27
* djahandarie goes that route24/02 05:27
copumpkinoho!24/02 05:31
copumpkina secret dependency!24/02 05:31
copumpkin