--- Log opened Wed Dec 01 00:00:20 2010
freiksenetwhat is the difference between "checking" that something has type a and infering that something has type a?01/12 12:50
freiksenetin type system sense. I dunno if agda does this distinction, pisigma seems to do01/12 12:51
Saizanfreiksenet: checking is when you're given both a term and a type as input, inference is when you're given only the term and you're supposed to deduce the type yourself01/12 13:14
freiksenetSaizan: ok, I thought so. Once again, thanks a lot.01/12 13:16
Saizanfreiksenet: np01/12 13:16
Saizanfreiksenet: http://lambda-the-ultimate.org/node/2340 <- this paper has a demonstrative implementation of a dep. typed language, btw01/12 13:17
freiksenetoh, thanks01/12 13:18
freiksenetthat's handy01/12 13:18
* franki^ spies Laney :o01/12 20:37
franki^...Although, Laney probably doesn't remember me, heh.01/12 20:47
* franki^ idles01/12 20:47
copumpkinstevan: I might make some changes to ctfp, reorganizing modules and such. I'll let you take a look before pushing it back to patch-tag in case you don't like it01/12 21:44
stevanalright :-)01/12 21:50
stevanit seems they might give the course again this spring btw, if so perhaps someone will extend it further :-)01/12 21:52
stevanfreiksenet: here's an other implementation btw: http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf01/12 22:05
freiksenetstevan: thanks, I'll take a look!01/12 22:06
freiksenetstevan: have you read the pisigma paper?01/12 22:09
stevanno, only scanned thru01/12 22:10
freiksenetI was just wondering about boxed terms and Rec type01/12 22:10
freiksenetwhether it was really needed to have them as core language constructs01/12 22:10
freiksenetor if they actually can be expressed through other constructs01/12 22:11
freiksenetat least Rec seems to be like that01/12 22:11
freiksenetand boxing seems to be like that in a language with a bit different semantics01/12 22:11
freiksenetam I missing something?01/12 22:11
stevani don't know to be honest01/12 22:12
stevanbut my impression is that they aimed for something pragmatic rather than minimal?01/12 22:13
freiksenetboth I think01/12 22:13
freiksenetstill. I am just trying to figure out the minimal subset needed01/12 22:14
stevanare you planing to implement something or?01/12 22:14
freiksenetkinda, yeah01/12 22:15
freiksenetjust playing around with some toy implementation01/12 22:15
freiksenetit has quite different semantics in other sense, that's why I am trying to split what is really needed and what is syntactic sugar01/12 22:16
freiksenetpity this research is still so novel so there is no #pisigma channel :D01/12 22:19
stevanok01/12 22:19
stevan:-)01/12 22:19
--- Day changed Fri Dec 03 2010
roconnordolio: is it easy to use that library to do proofs that rely on free theorems?03/12 20:21
freiksenetas I understand non-total languages with dependent types type-check them through (partial) evaluation03/12 20:22
freiksenethow would they handle the situation when term can't be evaluated without runtime information? eg user input based03/12 20:23
roconnorfreiksenet: every term has some normal form, even if it is a lambda expression.03/12 20:23
freiksenetroconnor: okay, how does that help in current situation?03/12 20:25
freiksenets/current/given03/12 20:25
roconnorall terms can be evaluated, whether or not input is available03/12 20:28
freiksenetcould you please elaborate? what if we have some (hypothetical) situation like a sigma type x:Char * case x of 'a' -> Foo | case x of 'b' -> Bar03/12 20:29
freiksenet(pisigma syntax, dunno how I would write that in agda tbh)03/12 20:30
roconnorokay03/12 20:30
freiksenetoh.03/12 20:31
freiksenetnow I see that03/12 20:31
freiksenetroconnor: thanks a lot03/12 20:31
roconnor:)03/12 20:31
dolioroconnor: Easier than figuring out what the parametricity statement yourself.03/12 20:35
roconnordolio: but is it easy to use the parametricity theorem?  I.e. I want to prove various theorems about polymorphic functions, but my proofs use parametricity, which isn't something that one can by default use in theorem provers.03/12 20:38
roconnordolio: (specifically I want to prove that my multiplate laws are equivalent the the laws of a coalgebra for a comonad :D)03/12 20:39
dolioWell, if you know roughly what the parametricity theorem should say, it's not that hard.03/12 20:39
roconnorI know exactly what my paratramecity theorems are.  Should I just take them as axioms?03/12 20:39
dolioYeah. Either postulate them, or take them as arguments to a module.03/12 20:40
dolioAnyhow, if you know what you're supposed to be filling into each hole for the theorem, it's not that hard. But I think the type prompts in the auto-generated stuff tends to be un-helpful if you don't.03/12 20:42
dolioAnd there are lots of implicit things, which can get confusing in large theorems.03/12 20:43
--- Day changed Sat Dec 04 2010
Eelisi can't seem to find anything in the reference manual about program extraction. does Agda support anything like that?04/12 19:01
copumpkincompilation?04/12 19:36
Eelisanybody else?04/12 19:45
edwinbas far as I know, only compilation...04/12 19:45
Eelisok, thank you.04/12 19:45
copumpkinlol04/12 19:46
edwinbif two people say it, it must be true ;)04/12 19:46
copumpkinwhat's the difference?04/12 19:46
copumpkinit only seems to be different if you attempt to separate proofs and programs04/12 19:46
edwinbI suppose an additional aim of extraction could be to produce readable, maintainable code04/12 19:46
copumpkinaha04/12 19:46
copumpkinagda definitely doesn't attempt to do that :P04/12 19:46
edwinbNo, I'm not convinced there's any value in it either04/12 19:47
freiksenetAs I understand agda uses types to "emulate" type classes. I read the Maybe source, and it has "functor" function defined04/12 20:51
freiksenetdoes it mean that you can use <$> on maybe?04/12 20:51
glguyI understand that it isn't Agda, but does anyone have the uagda tarball handy? (server is down for building maintenace)04/12 21:05
Saizanglguy: is that the same as miniagda? http://www2.tcs.ifi.lmu.de/~abel/miniagda/index.html04/12 21:17
Saizanfreiksenet: yes, after you open the RawFunctor (or even RawMonad) passing it the "functor" record04/12 21:18
freiksenetSaizan: ok, I see.04/12 21:19
freiksenetSaizan: how would one define something like "binary", where binary is a list of naturals, but naturals can only be 0 or 1?04/12 21:19
freiksenetwould it be something like List of Fin 1?04/12 21:28
dolioFin 1 has only one element.04/12 21:44
dolioFin 2 has 2 elements.04/12 21:44
freiksenetoh, ok04/12 21:44
sullywhat is uagda?04/12 21:44
lispy_sully: http://www.reddit.com/r/dependent_types/comments/efb3y/micro_agda_a_simplistic_language_with_native/04/12 22:24
--- Day changed Sun Dec 05 2010
copumpkinis there a mechanical way to get a fold out of a church encoding of a type?05/12 05:40
copumpkinit seems like there should be05/12 05:40
dolioA Church encoding is a fold.05/12 05:42
copumpkinoh well, I meant the one-level-deep thing05/12 05:43
copumpkineliminator?05/12 05:43
copumpkinunlist :: List a -> r -> (a -> List a -> r) -> r05/12 05:43
Saizanyou can implement that with foldr, but it's O(n)05/12 05:45
copumpkinbut vice versa?05/12 05:45
Saizanvice versa you don't lose efficiency, but you need a separate source of recursion (e.g. fix)05/12 05:46
copumpkinhmm05/12 05:47
Saizananyhow that's one of the reasons primitive eliminators are para- rather than cata- morphisms05/12 05:47
copumpkinso if I want to only allow primitive recursion, but also support pattern matching-alike things with a "one-level eliminator", I'd need to generate both a fold and the flat thing for each type?05/12 05:47
Saizanno, you generate only the paramorphism from which you can implement a O(1) flat thing05/12 05:49
copumpkinprimitive eliminators where are para?05/12 05:49
copumpkinhm05/12 05:49
Saizanwell, the usual induction principles, like (P : Nat -> Set) -> P zero -> ((n : Nat) -> P n -> P (suc n)) -> (n : Nat) -> P n05/12 05:50
Saizanin the recursive case you are given the immediate substructure 'n' as an argument05/12 05:50
copumpkinoh, so that's a para?05/12 05:50
copumpkinI'd never really seen it that way05/12 05:50
copumpkinhmm05/12 05:51
Saizanit fits the paramorphisms from category-extras if you take P = \ _ -> r05/12 05:51
copumpkininteresting05/12 05:52
Saizanserialization of interface files uses Data.HashTable?05/12 16:46
copumpkinthat seems odd :P05/12 16:52
Saizan"[Agda] .agdai serialisation runs into segfault in Data.HashTable"05/12 16:53
Saizani guess not everyone got the news from harrop :)05/12 16:54
copumpkinlol05/12 16:55
--- Day changed Tue Dec 07 2010
copumpkinSaizan: so an "induction principle"/eliminator is a paramorphism in general? what about for non-recursive types?07/12 04:32
copumpkinI guess non-recursive types are just constant fixed points07/12 04:32
Saizanwell, not that i've seen any literature make that connection, but that's the structure07/12 04:33
Saizanand yeah, non-recursive types are just a degenaration07/12 04:34
dolioelim-Nat s z zero = z ; elim-Nat s z (suc n) = s n (elim-Nat s z n)07/12 04:36
dolioSo the computational rules are what you'd expect for a well-optimized paramorphism, too.07/12 04:37
dolioOr, directly implemented. Or whatever.07/12 04:39
--- Day changed Wed Dec 08 2010
glguyIs there any way to show that this (or even that its double-negation) is true in Agda?08/12 22:21
glguydemo : (f : (A : Set) → Maybe A) → (A : Set) → f A ≡ nothing08/12 22:21
Saizanno08/12 22:29
--- Day changed Fri Dec 10 2010
jonrafkindagda 2.2.8 doesnt seem to build for me, i get to test 127/199 and then it says 'ExitFailure 9'10/12 18:45
jonrafkindill try building from darcs..10/12 18:58
--- Day changed Sat Dec 11 2010
Saizanpigworker: http://personal.cis.strath.ac.uk/~conor/fooling/Nobby.agda <- for nm here, there's some precondition to impose on the Nat and the ones in the Env G to avoid variable capture, right?11/12 16:03
pigworkerSure. You have to kick off the Nat with a fresh number.11/12 16:05
pigworkerIndeed, a number higher than all others used so far.11/12 16:06
Saizanif so far refers only to the ones in the environment i think i've a counterexample11/12 16:39
Saizanhttp://hpaste.org/42246/nm_test11/12 16:40
Saizannormalizing with that environment should produce a term with 2 free variables, afaiu11/12 16:41
pigworkerI can't remember how any of this worked. I'll stare a moment.11/12 17:06
pigworkerYeah, I see the bug. It's where ev kicks off the name supply in unq.11/12 17:14
Saizanyeah11/12 17:15
Saizani guess ev needs to receive a separate name supply too11/12 17:16
pigworkerI hope not.11/12 17:17
pigworkerI think I need to allow neutral functions in the model, and then get rid of unq altogether.11/12 17:31
pigworkerFunnily enough, I do something of the sort in DepNobby.11/12 17:33
Saizanbut then the normal forms won't be eta-long anymore?11/12 17:39
pigworkerquote has to do more eta-expansion, when you set it up that way11/12 17:40
pigworkerTry http://personal.cis.strath.ac.uk/~conor/fooling/Nobby2.agda11/12 17:57
pigworkerIn that version, values are either "active" or quotation process awaiting a name supply. Value application runs active functions and grows inactive functions by quoting the given argument.11/12 18:00
pigworkerBy the way, those who believe de Bruijn indices are for cyborgs only may be mildly amused by this http://personal.cis.strath.ac.uk/~conor/fooling/Jigger.agda (which I just cooked up).11/12 18:02
* Saizan reads11/12 19:27
Saizanjigger is pretty cool!11/12 19:35
Saizani was afraid one'd have to resort to something much more heavyweight for that11/12 19:36
lispypigworker: I looked at it, but the value is not immediately obvious to me (I need an explanation!)11/12 19:37
pigworkeram currently trying to kick jigger into SHE-haskell, but having a bad time...11/12 19:38
pigworkerlispy: Jigger turns object-level variable binding into meta-level variable binding (so you can use a name!), even though syntax is de Bruijn (so there's no alpha conversion misery)11/12 19:41
lispypigworker: ah11/12 19:42
pigworkerThe trick is to represent a variable by a function which computes the correct index in any large enough scope.11/12 19:42
lispypigworker: so a lot of the magic is in the type of l?11/12 19:43
Saizanit seems inference works less well when constructing open terms11/12 19:43
pigworkerexactly11/12 19:43
lispypigworker: do you frequently prototype in agda and translate to SHE?11/12 19:44
pigworkerSaizan: it's quite sensitive to constraint solving...11/12 19:45
pigworkerlispy: yes11/12 19:45
* pigworker nips to the shops11/12 19:46
BoxoI don't understand this http://pastebin.com/AY1KgngB11/12 20:59
Boxofixed: http://pastebin.com/0qjE7tFW11/12 21:01
BoxoThey look like they're the same thing, but in agda, A f : Set1, while in haskell, A f :: *11/12 21:02
SaizanGHC haskell allows impredicative polymorphism since the type system is inconsistent anyhow11/12 21:05
pigworkerHaskell lets you write datatypes which make no logical sense.11/12 21:05
BoxoSo... Is this nevertheless the way to do typeclasses in agda? http://pastebin.com/5kyMsaxp11/12 21:09
Saizanthere's RawFunctor in the "standard library" which is a renaming of that11/12 21:10
BoxoRight. So why doesn't that datatype actually make no sense? What to read?11/12 21:11
Saizanit makes sense, it just has to be in Set111/12 21:11
Saizanit'd make less sense if it was in Set, because it'd be quantifying over itself, which is also something you can use to prove false (though i'm not sure if the construction would work with FunctorI itself)11/12 21:14
Saizanit's Hurkens' paradox iirc11/12 21:17
--- Day changed Sun Dec 12 2010
Saizanheh, i wanted to show pigworker that jigger-like constraints are nicely solved with typeclass hackery http://hpaste.org/42263/brujin_with_class12/12 04:20
pigworkerSaizan: Thanks for that! I'll borrow it, if I may. I was trying a more direct translation of the Agda, but ghc (6.12.1, so old news?) makes dangerous assumptions about how to check types involving quantifiers and type families and thus fails to check types it can infer. Going via a Leq relation avoids the problems I'm having with addition.12/12 11:01
Saizanpigworker: sure :)12/12 15:36
Saizanpigworker: yeah, addition didn't seem workable with ghc-6.12, though with ghc-7's new constraint solver it might be much better12/12 15:37
pigworkerIt got quite close, but there is an issue with the way ghc 6.12 (and perhaps others) checks types of form (forall x. t). If it's checking against (forall y. s), it fixes x and tries to solve for y by unifying s with t. This can fail if s and/or t contain non-injective functions, even if s is *exactly* t[y/x]. Frustrating.12/12 16:01
Saizando you still have the code that shows that problem?12/12 16:04
pigworkerSaizan: http://personal.cis.strath.ac.uk/~conor/fooling/Jigger.lhs is as far as I got. The commented out type on "varp" is inferred but not checkable.12/12 16:27
pigworkerTo be fair, I bet there are types (forall x. t) such that for some s other than x itself, t[s/x] = t, e.g. if t invokes (Even x) and we take s to be (S (S x)). If the question is not "is this one of those?" but "how can this be instantiated to make one of those?", we might get multiple solutions.12/12 16:33
Saizanghc-7 gives clearer error messages, which point to the fact that since 'n' appears only as argument of a type family it won't conclude the inferred one has to be the same as the one in the type singnature12/12 17:12
pigworkerok, so the problem is one of omission -- there seems no direct way to pass polytyped values at their exact polytype12/12 17:26
pigworkermeanwhile, I've now fitted your overlapping-instance style jiggerer to my new toy typechecker; so far so good12/12 17:27
Saizanyeah, ghc lacks a true type lambda/type application, you need to add so-called phantom arguments12/12 17:37
Saizan(quite fun that OverlappingInstances seem to only be useful for typeclass hackery)12/12 17:40
pigworkerI've hit my next ghc weirdness. Can I beg a ghc-7 opinion? (I don't want to touch my installation of anything until term is over; then I'm nuking it.)12/12 18:11
Saizanpigworker: ok12/12 18:11
pigworkerhttp://personal.cis.strath.ac.uk/~conor/fooling/Spiny.lhs  has an issue...12/12 18:14
pigworkerI supplemented the lifting jiggery with some functional pokery, in an attempt to apply variables like functions, but I'm somehow losing polymorphism in 6.12.12/12 18:16
Saizanhttp://hpaste.org/42271/error <- 7 gives the same error12/12 18:17
pigworkerthanks... hmmm12/12 18:17
Saizanit works if you add t to the forall n in ->>'s signature12/12 18:20
pigworkerD'oh!12/12 18:20
Saizanheh, i think it's the first time i see a bug caused by implicit foralls12/12 18:21
copumpkinimplicit foralls are the devil!12/12 18:22
pigworkerno, they're the angel!12/12 18:22
copumpkinpigworker: what are you making?12/12 18:22
pigworkera pig's ear12/12 18:23
copumpkintasty12/12 18:23
pigworkerI'm trying to cook up an entirely first-order term representation (locally nameless) which I can still program with (implementing operators on values, etc).12/12 18:26
pigworkerThe extra foot on the floor is that I want to be able to force (by Haskell typing) that a term is beta-delta-head-normal.12/12 18:27
copumpkinthat sounds tough :)12/12 18:28
pigworkerExcluding redexes isn't so tricky if you go with a spine representation.12/12 18:30
pigworkerI think this is now a job for #epigram...12/12 18:37
--- Day changed Mon Dec 13 2010
copumpkinedwinb: epic work!13/12 17:25
Saizan?13/12 17:25
edskoquick syntax question, if anyone is around: what does _.g mean?13/12 17:26
Saizanthat appears in a goal?13/12 17:26
edwinbI wonder if I might one day regret that choice of name...13/12 17:27
edskoyeah ,I have a hole with a very big type, and somewhere inside that type is the expression _.g ; but if I abstract out that goal as a separate function (and add all the available hypotheses as arguments) then Agda complains ".g is not a valid expression@13/12 17:27
kosmikusedwinb: :)13/12 17:28
Saizan.g alone is when it's referring to an implicit argument, so if you want to really refer to that you first have to bring it in scope with a {} pattern somewhere13/12 17:29
Saizan_.g though sounds like it's referring to some locally defined g, and _ is the name of that local module13/12 17:29
edskohere's part of the type of the goal:13/12 17:31
edskoGoal: Σ (proj₁ f)13/12 17:31
edsko      (λ x →13/12 17:31
edsko         proj₁13/12 17:31
edsko         (iter η μ13/12 17:31
edsko          (λ x' →13/12 17:31
edsko             Σ (proj₁ x' → proj₁ X)13/12 17:31
edsko             (λ x0 → proj₁ (proj₂ x' (λ x1 → proj₂ X (x0 x1))))13/12 17:31
edsko             ,13/12 17:31
edsko             _.g (proj₁ x' → proj₁ X)13/12 17:31
edsko             (λ g' → proj₂ x' (λ x0 → proj₂ X (g' x0))))13/12 17:31
edsko          (proj₂ f x))) →13/12 17:31
edskothree lines from the bottom13/12 17:31
edskowe have g  : proj₁ X → proj₁ Y available as an assumption13/12 17:31
edskoso not .g (it's not an implicit argument)13/12 17:32
edskotype is horrible, I know, that's what I'm trying to figure out; but I don't understand what that _.g means13/12 17:32
Saizanme neither :\13/12 17:33
edskohm, bummer :)13/12 17:34
edskooh, hm. renaming the explicit argument "g" to "foo" does not change that _.g one bit.13/12 17:35
copumpkina terrible autogenerated name?13/12 17:36
copumpkin:P13/12 17:36
edskoah.13/12 17:36
edskoit comes from13/12 17:36
edskoμ : {D : Set1} -> Fam (Fam D) → Fam D13/12 17:37
edskoμ {D} (A , B) = (Σ A (proj₁ ∘ B) ,  g)13/12 17:37
edsko                where g : Σ A (proj₁ ∘ B) -> D13/12 17:37
edsko                      g (a , k) = proj₂ (B a) k13/12 17:37
edskosomewhere up in the module13/12 17:37
edskowhen I change that "g" to "bar" then the "_.g" changes to "_.bar"13/12 17:37
fdsIs this channel too intellectual for pastebin? ;-)13/12 17:37
copumpkinoh yeah, that's how it does wheres13/12 17:37
copumpkinI hate it :P13/12 17:37
copumpkinwhere blocks are the devil in agda13/12 17:37
edskoright, ok, well, that solves that anyway, thanks13/12 17:38
edskofds: sorry, should I avoid copying and pastnig in bits of code? not very familiar with IRC etiquette :)13/12 17:38
Saizanit's better to put them on a site like hpaste.org or pastebin.com ..13/12 17:39
fdsLong pieces of code (more than two or three lines) are usually put on some site like the ones that Saizan mentioned13/12 17:40
edskook, fair enough. will do in the future :)13/12 17:40
Saizanit's less of a problem if the channel is as slow as it currently is :)13/12 17:40
fdsIndeed13/12 17:42
fdsSo, out of interest, where are you guys? I'm here because I was interested in applying to Chalmers, but it looks like that isn't happening, for bureaucratic reasons.. I don't suppose any of you are at UK institutions are you?13/12 17:43
* edwinb waves from Scotland13/12 17:44
fdsCool, which uni?13/12 17:44
* fds is looking for places to apply to next year13/12 17:45
edwinbI'm at St Andrews13/12 17:45
edwinblooking for undergrad or postgrad?13/12 17:45
kosmikusI'm in .de13/12 17:46
fdsPostgrad, I've got a BSc in maths, and I've taken two years out to work as a "programmer" (PHP T_T) slash English teacher... now I'm looking for an interesting MSc13/12 17:46
edwinbaha13/12 17:47
edwinbwe have a taught MSc, and it'd be nice to have people to do dependent type related projects for it...13/12 17:47
kosmikusfds: are you looking for dependent types in particular, or more generally functional programming?13/12 17:47
fdskosmikus: Functional programming in general, I guess. I'm not really an expert programmer, heh. But I mostly write Scheme at the moment, and would like to continue in that direction, if possible.13/12 17:48
kosmikusfds: I can certainly recommend the "Computing Science" master program at Utrecht University in .nl. They have a functional programming "track". There are courses like Advanced Functional Programming or Compiler Construction (using FP) in the program, and thesis topics in that area too.13/12 17:54
fdskosmikus: Thanks, I'll definitely look into that!13/12 17:55
edwinbAlas, I can't compete with that...13/12 17:56
edwinbbut we have a good research group if you want to take it further ;)13/12 17:56
kosmikusedwinb: yes, but you have Idris :)13/12 17:56
edwinband Hume!13/12 17:57
kosmikusedwinb: and alas, I can no longer compete with that either ...13/12 17:57
edwinbkosmikus: are you at Well-Typed now?13/12 17:57
kosmikusyes13/12 17:57
fdsHa, well, UK universities might be more welcoming to me, seeing as I'm a British citizen. I don't know, maybe they won't. Univeristy admission is a dark art to me.13/12 17:57
edwinbnot so much time for Agda hacking then, presumably...13/12 17:57
kosmikusfds: admission to Utrecht shouldn't in general be a very difficult problem.13/12 17:58
kosmikusfds: living in NL isn't a problem when knowing only English. and courses are all in English anyway.13/12 17:59
kosmikusfds: housing (even student housing) in a combination with the tuition fee can be a financial strain however.13/12 17:59
fdskosmikus: Cool, I'd love to live in the Netherlands, or anywhere else in Europe, actually. I'm quite bored by the prospect of going back to the UK. (I'm living in Mexico at the moment.)13/12 18:00
fdskosmikus: Yes, I'm still not sure about how I'm going to finance any of this, but I'm hoping I can get some help from my family... :s13/12 18:00
kosmikusedwinb: no, not so much. but still a bit of research time, and I'm actually optimistic that once I'm settled more, it'll be possible to do some research.13/12 18:00
kosmikusedwinb: I certainly have plans going to AIM and to ICFP.13/12 18:01
edwinbexcellent13/12 18:01
fdsTuition fees seem to be lower in the NL than in the UK13/12 18:04
kosmikusfds: yes, they're probably lower than in the UK, at least for people from the EU13/12 18:08
fdsHm, my problem is that the Dutch application process, like the Swedish application process and I guess everyone else's, requires `certified' copies of my certificates. Unfortunately I can't afford to pay a notary public at the embassy here and my awarding institution is on the other side of the Atlantic! But, I'm getting incredibly offtopic here and I should be working, thanks for your advice. :-)13/12 18:32
kosmikusfds: is it *that* expensive to make "certified" copies elsewhere? in .de it's usually something like 1 or 2 EUR per page, which is affordable, I think. but perhaps you can just ask your awarding institution to make new copies for you by sending them an email, even if it's far away?13/12 23:47
fdskosmikus: http://ukinmexico.fco.gov.uk/en/help-for-british-nationals/living-in-mexico/how-legalise-document says £25 for a certified copy of my passport and that I should ask the British council about educational documents, I'm at work now so I'm not going to search through their site! I shall email my university tonight though and see if they can do something for me. :-)13/12 23:52
fds(Thanks for taking an interest, by the way)13/12 23:52
fdsAnd, for the record, I have three or four documents that need "certifying"13/12 23:52
fdsAlso, I'd have to go to Mexico City. But, we'll see.13/12 23:53
fdsI'll figure something out!13/12 23:53
* fds is determined13/12 23:53
--- Day changed Tue Dec 14 2010
edskoanybody around for a quick style question?14/12 10:46
edskois the only way to pattern match the 'with' clause?14/12 10:54
kosmikusedsko: I assume you mean pattern match on a rhs? Yes, the "with" clause it the only syntactic construct to do that. You can, however, also use a local definition to perform pattern matches, and afaik, with-clauses are internally desugared into local definitions.14/12 11:17
edskogets a bit apinful though14/12 11:18
edskoI have a goal of shape14/12 11:19
edskoGoal: proj₁ (iter η μ .. (FJ j))14/12 11:19
edskoand in my environment an assumption14/12 11:19
edskop-≡ : FJ j ≡ ι o14/12 11:19
edskosorry, that's an equivality proof over FJ j, not sure you can see the unicode symbols (I cannot)14/12 11:20
edskoa "rewrite" on that proof would simplify the goal to a point where the proj1 can be resolved14/12 11:20
edskobut I cannot do that rewrite unless I introduce an auxiliary function14/12 11:20
edskosince the goal is a 'subterm':14/12 11:20
edskoaux₁ {I} {O} (J , FJ) {X} {Y} g g* (j , fj) | ι o with-≡ p-≡ | .(ι o) | refl = (j , {! !} )14/12 11:21
edskothis is a dependent pair14/12 11:21
edskoand before I specify the first component (j)14/12 11:21
edskoI don't have the necessary equality14/12 11:21
edskonot sure I'm making any sense..14/12 11:21
danredsko: I can see your unicode symbols :)14/12 12:46
edskothat's not fair :)14/12 12:48
freiksenetwhen HM-typed language tries to auto-infer type of some function \x -> t, it assigns a type variable to x, collects constrains with x in the scope and then unifies them. How would a depedendently typed langauge like Agda do the same thing? non-dependent types only in this case14/12 12:54
freiksenetdoes agda collects constraints and unifies them too or maybe there is some other way?14/12 12:56
pigworkerfreiksenet: certainly, Agda collects constraints and unifies them (with Miller's higher-order pattern unification, rather than Robinson's first-order unification); also, it's usually the case that \x -> t is being *typechecked*, which is a much easier game14/12 13:48
freiksenetI know14/12 13:49
freiksenetthat's why I am asking )14/12 13:49
freiksenet(I mean I know that type checking is easier)14/12 13:49
freiksenetpigworker: thanks14/12 13:50
pigworkerIt's certainly not hopeless to generate fresh unknowns S : Set, T : S -> Set and try to check x : S |- t : T x, but there are no guarantees14/12 13:51
freiksenetok14/12 13:52
pigworkerThose problems do get harder if you have subtyping/cumulativity in the picture.14/12 13:53
freiksenetbecause constrains become "one-way"?14/12 13:53
freiksenetconstraints*14/12 13:54
pigworkeryeah14/12 13:54
pigworkerusage type, even if known, just bounds rather than determining definition type14/12 13:55
pigworkerIt's also murder if you're trying to guess whether there are any hidden arguments as well as the explicit \x -> t.14/12 13:56
freiksenetwell I guess when we are infering we can assume that there are no hidden arguments14/12 13:56
pigworkerit's not always that clear cut14/12 13:57
pigworkeris inferring the same as checking an unknown type?14/12 13:57
freiksenethmm.14/12 13:58
freiksenetwell not really14/12 14:00
freiksenetwhen checking for unkwown type we just need to check if it works for _some_ type, while inferance tries to get that type?14/12 14:00
pigworkerWhat should happen if we are checking \x -> T against some unknown Z : Set ? Do we wait for Z to be solved with a Pi-type, or do we try to infer the function type and then solve Z? Either way can have bad consequences.14/12 14:01
pigworkerSuppose other constraints in the typechecking problem involve Z.14/12 14:03
freiksenetagda does the latter?14/12 14:05
pigworkerI don't know, but it shouldn't be hard to find out.14/12 14:06
pigworkerThe danger if you decide it's an inference problem and make the simplifying assumption that there are no implicit arguments, it may happen that some other constraint determines that Z = {y : Y}(x : S y) -> T y x. Unforced moves are always dangerous, but so is deadlock.14/12 14:09
freiksenetwhat can be done to mitigate this problem?14/12 14:10
pigworkerMy plan is to get rid of {x : S} -> T as a type in the theory, allowing it only as an elaboration convention established by explicit signatures in source code. That would validate the simplifying assumption.14/12 14:15
freiksenetdo you mean getting read of implicit arguments or getting rid of pi types?14/12 14:15
freiksenets/read/rid14/12 14:16
freiksenetI assume the former, but just to check14/12 14:16
pigworkerI mean that {x : S} -> T should no longer be a type, but (x : S) -> T should still be ok. Explicit "type signatures" f : {x : S} -> T would declare some elaborated thing f' : (x : S) -> T and establish the convention that the source syntax f elaborates to f' x, for some fresh unknown x.14/12 14:19
freiksenetokay14/12 14:19
pigworkerThat way, implicit arguments become part of the elaboration process, but they stay out of the type theory.14/12 14:20
freiksenetyeah, that sounds good.14/12 14:20
pigworkerSome functionality is lost in the corners. Some clarity is gained. I hope it's a good trade. I'll certainly do the experiment.14/12 14:20
freiksenetwhat I am currently doing is small experiment with pi types represented as something like (x : Set) -> (x -> Set)14/12 14:23
freiksenetbut this way it would be nice to make it possible to have direct lambda definitions which are infered14/12 14:23
freiksenetthat's why I was asking about the best way to infer non-dependent functions14/12 14:24
pigworkerMiller unification will get you a long way.14/12 14:24
freiksenetpigworker: ok. thanks14/12 14:27
pigworkerI'm not sure I trust any of the existing implementations of implicit arguments, so light in this area is a contribution. Soundness (no bad terms generated) would be nice. Independence of the order of refinements is, however, the goal.14/12 14:34
dantenwohoo Epic support in darcs repo14/12 16:42
danrreally? :)14/12 16:43
danrcongrats14/12 16:43
dantenYes just got a mail from Ulf14/12 16:43
dantenactually it went in yesterday but now we have a slightly updated version14/12 16:43
danrwhen's the paper coming? ;)14/12 16:44
dantenheh, we are going to put up the report after we made some changes, probably later tonight14/12 16:45
dantenwith some epic factorial benchmarks..14/12 16:45
kosmikusgreat! I didn't even know you are working on that ...14/12 16:47
danten:) yeah we have worked on it in during a course here at Chalmers. We will continue with it as a Master during the spring14/12 16:49
Saizan_does it still support calling into Haskell?14/12 16:52
dantenNo, we added a new pragma which for adding epic code. Well epic can call c functions so I suppose you could get haskell functions that way...14/12 16:53
kosmikuswhat evaluation strategy does epic use?14/12 16:55
dantenbut the COMPILE pragma and COMPILE_EPIC (what we called ours) can be used at the same time so hopefully the standard library can use both14/12 16:55
dantenit is strict but it has a special expression to make expressions lazy14/12 16:56
kosmikusok14/12 16:56
dantencurrently we only use lazy when calling function with coinduction, and it seems to work(tm)14/12 16:56
kosmikusI'm looking forward to it14/12 16:57
danten:)14/12 16:57
dantenAnyone with a mac or knows how to install stuff on it? :)14/12 21:07
Adamanthttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX14/12 21:11
dantenBasically Im trying to figure out how to install epic14/12 21:12
dantenI don't have a mac but it becomes a problem for people that do14/12 21:13
Adamantah14/12 21:13
Adamantyou probably want to create a package14/12 21:13
Adamant.mpkg or .pkg14/12 21:13
dantenhmm14/12 21:13
AdamantI assume epic is a compiler deal14/12 21:13
Adamantthat will install it as a Unix app for use on the system14/12 21:14
Adamantsomething like a IDE would probably be better as a bundle that you put into Application14/12 21:14
Adamantyou could also use MacPorts14/12 21:15
dantenThere exists cabal package for epic on hackage, but it requires Boehms gc and GMP, but these should already be in macports right?14/12 21:16
edwinbyes, "boehmgc" and "gmp"14/12 21:16
edwinbalthough I gave up on macports and install things by hand now14/12 21:17
dantenah ok, well as I don't have a mac Im kinda lost14/12 21:17
edwinbfortunately, I do ;)14/12 21:18
dantenyay! :D14/12 21:19
edwinbA version of epic without those dependencies is on my TODO list14/12 21:21
edwinbunfortunately, quite low14/12 21:21
edwinbbut it would make a few things a lot easier14/12 21:21
dantendo you have any plan on compiling to llvm?14/12 21:25
edwinbyes. "Eventually"14/12 21:26
edwinbI might have a go in the new year14/12 21:26
edwinbI think it might get more important for some systems programming stuff I want to try with Idris14/12 21:26
edwinbusing C as a target is just too limiting14/12 21:27
edwinbalthough it works pretty well usually14/12 21:27
dantenwe have had some problems that we are getting segmentation faults due to that we ran out of stack space. Maybe llvm can perform better in that regard14/12 21:28
edwinbinteresting. Very deep recursion?14/12 21:28
dantenyes14/12 21:28
edwinbif your functions are tail recursive gcc should optimise that away14/12 21:28
dantenwe wrote an interpreter for a simple language and had factorial in it, we were only able to compute fac 8 before it failed14/12 21:29
edwinb8 as a Nat or an Int?14/12 21:29
dantenBigInt14/12 21:29
edwinbthat's a bit worrying14/12 21:29
dantenwe compile all Nat-like as BigInt14/12 21:29
dantenit could be the eval function that does a lot of stuff.14/12 21:30
dantensince we are interpreting fac etc.14/12 21:30
edwinbah, I see14/12 21:30
dantenhttp://hpaste.org/42335/prf_in_agda14/12 21:32
dantenwhat is also sad is that MAlonzo is faster in this example14/12 21:32
edwinbDo you have the epic code for that example?14/12 21:33
edwinbIf MAlonze is faster I'd consider that a bug ;)14/12 21:33
danten:p14/12 21:33
dantenwait14/12 21:33
edwinbI'd be interested to know how MAlonzo compares in general though14/12 21:33
dantenwe have only done this experiment and the normal factorial (where MAlonzo don't perform well at all)14/12 21:34
edwinbI'm just wondering if there might be some way you're using epic that I haven't thought of that I could easily optimise...14/12 21:35
dantenhttp://hpaste.org/42336/prf_in_agda_annotation14/12 21:36
dantenthat is very possible14/12 21:36
dantenwe use a lot of worker/wrapper and inline annotation14/12 21:37
dantenalso everything is compiled in one module and get very easy to recognize names14/12 21:37
edwinbit all seems reasonably sane to me14/12 21:42
edwinbI'll see if I can compile it here and see what happens...14/12 21:42
edwinbcor, the stack gets 74869 deep before it gets fed up with factorial of 914/12 21:49
dantenit is probably the rec construct, since eval for it isn't tail recursive in the argument.14/12 21:51
ollepollethat is still less than 9!, which I would guess would be the order of the expected stack depth (since it's using rec)14/12 21:52
edwinbI'm having trouble profiling it because it runs too quickly...14/12 21:52
edwinbI wonder if MAlonzo is taking advantage of GHC being clever14/12 21:53
edwinbof course this would be an advantage of compiling to Haskell14/12 21:54
dantenMAlonzo took 1.194s and Epic took 3.040s for fac 9 on ollepolle's computer14/12 21:56
edwinbwow, that's a big difference14/12 21:57
edwinbI would not be at all surprised if the culprit was the big number arithmetic14/12 21:57
edwinbbut I wouldn't like to say anything until I've profiled it properly14/12 21:58
dantenoh yeah, the Integer type in Haskell is Int for small values right?14/12 21:58
edwinbthere's an awful lot of probably needless memory allocation going on14/12 21:58
edwinbsee, I've never used them ;)14/12 21:58
dantenbut it seems that MAlonzo converts between Integer and a ADT for Nat14/12 21:59
dantenhehe14/12 21:59
edwinbdoes it convert once, or regularly?14/12 22:00
dantenhmm maybe it only convert it once from the literal.14/12 22:00
dantenhaving a hard time understanding all these coercion stuff :p14/12 22:03
dantenbut it seems like eval always works on the ADT14/12 22:04
edwinbits advantage is that it won't have to allocate every time it makes a new number, just get a pointer to the smaller number14/12 22:04
edwinbwhereas subBig allocates a new number every time14/12 22:05
edwinband allocation is expensive14/12 22:05
* edwinb tries a little experiment...14/12 22:06
edwinbhmm, yes, it runs 5 times faster with Int rather than BigInt14/12 22:12
dantenahh ok14/12 22:13
edwinbsuggests BigInt needs work14/12 22:13
edwinbbut I think that's my problem rather than yours...14/12 22:13
dantenso we want to have Int that can magically upgrades to BigInt14/12 22:13
dantenor something like that14/12 22:14
ollepolleI'm not that familiar with libgmp, but isn't that what it does?14/12 22:14
edwinbI think the problem is most likely that epic allocates a lot more than it should14/12 22:14
edwinbI'll profile properly before reaching any conclusions though14/12 22:16
dantenwasn't it that everything that is allocated gets reallocated for the gc or something like that?14/12 22:16
dantenwhen using foreigh call14/12 22:17
edwinbno, it just uses foreign pointers and lets the foreign function deal with allocation14/12 22:17
edwinbthe problem here is that a new GMP integer gets allocated every time you do a computation14/12 22:18
dantenbut the return value of those functions14/12 22:18
edwinband you do a lot of them14/12 22:18
ollepollehow does the haskell backend avoid the reallocation?14/12 22:19
dantenI just remember we had to do something special when returning stuff we had allocated inside c-functions14/12 22:19
edwinbthe haskell backend isn't using GMP, and presumably the unary representation isn't big enough to cause any major problems in this example14/12 22:19
dantencurrently when it is N = Z | S N, when it has S n, it can just return n which is already allocated14/12 22:20
edwinbah, if you allocate stuff in C you need to arrange for it to be garbage collected somehow, yes14/12 22:20
ollepolleah, right14/12 22:20
ollepolleso essentially, it's more efficient to use the ADT constructor representation in this example14/12 22:20
edwinboddly, it seems that way14/12 22:20
edwinbbut only because my usage of GMP is rubbish ;)14/12 22:21
ollepollewell, it is doing primitive recursion for addition which is used inside the primitive recursive function for multiplication which is used inside factorial14/12 22:21
edwinbah... you aren't converting plus and mult to GMP operations are you?14/12 22:22
edwinbso I bet that's really expensive14/12 22:22
dantenwell since we are interpreting a language inside agda we can't really see that those add and mul are really add and mul. We do it for BUILTIN14/12 22:23
edwinbindeed. For Idris I do the conversion for plus and mult but I don't do any analysis beyond that14/12 22:23
dantenso ordinary factorial can do fac 10000 quickly14/12 22:23
ollepollethe factorial using BUILTIN is, btw, really fast14/12 22:24
edwinbit does rely on plus and mult being the right things14/12 22:24
ollepollethe example is still interesting though, since the haskell backend would face the same problems14/12 22:24
ollepolleIMO14/12 22:24
edwinbindeed14/12 22:24
dantenbasically we did this for two reasons: 1 I already had the code from a different course, 2) it contains Vec, Fin and Nat in an interesting way14/12 22:25
edwinbit's a nice stress test I think14/12 22:25
edwinbthere's quite a bit going on - inductive families, variable length argument lists14/12 22:26
edwinba bit of erasure14/12 22:26
dantenyeah without removing the forced arguments to the constructor we go from 3.040s to 3.930s so removing them is quite the win.14/12 22:27
edwinbI notice, by the way, that in doing the erasure you're occasionally left with undefined variables14/12 22:27
edwinbin that you use them, but they've been erased14/12 22:27
edwinband so using them is harmless since they don't do anything14/12 22:27
edwinbI only mention this because I've just made epic check for this by default14/12 22:28
ollepolleoh, that sounds like something we have to look into14/12 22:28
edwinbepic -checking 0 will turn it off14/12 22:28
dantenhmm something slightly weird there, our hope is that we since the function that is not marked [ERASED] will be inlined and all those variables should dissapear. But I think we substitute them for unit first, maybe we have a bug there.14/12 22:30
dantenin the recursive step etc.14/12 22:31
--- Day changed Wed Dec 15 2010
glguyIs it the case that this cannot be proven in Agda?15/12 01:12
glguymp : (φ : ℕ → Set) → ((n : ℕ) → Dec (φ n)) → Stable (∃ φ)15/12 01:12
SaizanStable P = ~~P <-> P ?15/12 01:13
glguyStable P = ¬ ¬ P → P15/12 01:13
glguythe algorithm that searches from zero up to the value that satisfies 'phi' would always terminate15/12 01:15
glguybut I can't imagine how you could convince agda of that15/12 01:15
sullyhrm15/12 01:16
sullygetting my IRC setup to be able to handle unicode seems like an important prerequisite for knowing what is going on in this channel15/12 01:16
Saizanyep15/12 01:17
glguyWhat client are you using that you have a manual configuration step?15/12 01:17
sullyI run irssi in a screen session, and my terminal emulator is xterm15/12 01:17
Saizani'm afraid you can only prove that it doesn't diverge15/12 01:17
Saizanso, is termination stable?:)15/12 01:18
glguyYou'd be asking the wrong person15/12 01:18
glguy;)15/12 01:18
sullyuxterm seems to not do anything differently...15/12 01:20
glguyyou have to tell screen to do utf-8 as well15/12 01:21
sullyit works if I use urxvt15/12 01:22
Saizanmaybe we can somehow use wellfounded recursion by saying that the difference between the current number and the searched one is getting smaller, though that seems hard without being able to touch this number15/12 01:25
* glguy switches networks15/12 01:29
doliomp stands for Markov principle?15/12 01:30
glguyyes :-D15/12 01:31
dolioThen I doubt it's provable in Agda.15/12 01:31
Saizanhttp://lambda-the-ultimate.org/node/4003 <- heh, continuations15/12 01:32
dolioYes, exactly.15/12 01:33
dolioAnd there's a subsequent paper by someone else (I think) that gets a language that validates ∀ x. ¬ ¬ P ↔ ¬ ¬ ∀ x. P15/12 01:34
dolioI think that's right, at least.15/12 01:34
dolioPerhaps it's only in one direction.15/12 01:35
* Saizan wonders if those let you write non-continuous functions15/12 01:35
dolioI doubt it.15/12 01:36
doliohttp://arxiv.org/abs/1012.092915/12 01:38
sullyvictory has been achieved.15/12 01:49
sullyexcept that I had to deal with X fonts, which is a major loss15/12 01:49
sullybut I won.15/12 01:49
edskoanyone around for one more syntax question?15/12 13:10
edskoif I have a type of shape ⟦_⟧₃ : {I O : Set1} -> (c : IR I O) -> {X Y : Fam I} -> (X ⇒ Y) → ⟦ c ⟧ X ⇒ ⟦ c ⟧ Y15/12 13:44
edskohow do I get the I into scope?15/12 13:44
dantenyou can do ⟦_⟧₃  {I = pat} stuff = ..15/12 13:45
edskoah, and not put any term inside the brackets you mean15/12 13:46
dantenyeah15/12 13:46
dantenits a little ugly but I don't know any other way15/12 13:47
edskook, unfortunate. but that works, thanks.15/12 13:47
edskothere is no way to write foo (a , b) = (b , a) as an anonymous function right?15/12 14:06
edskosomething like  λ (a , b) → (b , a) I guess15/12 14:06
dantenno you can't pattern match in lambda, you can define such a function in a where clause15/12 14:14
edskook, pity.15/12 14:14
edskothanks15/12 14:15
pigworkeredsko: I usually equip Sigma with its eliminator...15/12 16:23
pigworkersplit : {A : Set}{B : A -> Set}{P : Sigma A B -> Set} -> ((a : A)(b : B a) -> P (a , b)) -> (ab : Sigma A B) -> P ab15/12 16:25
pigworkerand then I can write   split \ a b -> (b , a)15/12 16:25
pigworkerProvided I'm partially applying split, Miller unification infers P!15/12 16:26
glguyeve mail to "errelay"?15/12 18:09
Mathnerd314statically-inferred type-level reference counting. has it been done, does it have a name, and if so do you have a link to a paper?15/12 22:48
copumpkinnot sure about reference counting, but maybe you'd be interested in region inference?15/12 22:49
copumpkin(for memory/scarce resource management?)15/12 22:49
Mathnerd314hmm, I haven't seen it15/12 22:51
copumpkinthere's a chapter on it in ATTaPL iirc15/12 22:51
copumpkinhttp://en.wikipedia.org/wiki/Region-based_memory_management15/12 22:51
copumpkincheck the inference section in there15/12 22:52
Mathnerd314hmm, not the same.15/12 23:02
Mathnerd314regions are lower-level.15/12 23:10
Mathnerd314I just want to annotate each value with the number of references to it15/12 23:16
Saizansounds like a variation on uniqueness and/or linear types15/12 23:29
Mathnerd314yeah, it's an extension15/12 23:55
--- Day changed Thu Dec 16 2010
djahandarielol dependent types16/12 00:13
copumpkinlol16/12 00:13
Mathnerd314wait, you're saying my type sounds like a dependent type?16/12 00:54
djahandarieUnrelated, lol16/12 00:54
--- Day changed Fri Dec 17 2010
jonrafkindim trying to run agda from the haskell prelude, what is a possibility to give for Agda.TypeChecking.Monad.Base.InteractionId ?17/12 09:07
Laneyhas anyone managed to typecheck the whole standard library? Seems to die on Data.Container.AltenativeBagAndSetEquality here17/12 10:54
Laney`make' in the root17/12 10:54
SaizanLaney: i managed in two or three runs17/12 12:06
--- Day changed Sat Dec 18 2010
danrwhat does it mean if a identifier begins with a . in a record? I cannot find that anywhere18/12 00:25
copumpkinmakes it irrelevant18/12 00:27
danrdo you mean irrelevant to supply when constructing a record?18/12 00:28
danror irrelevant in what sense?18/12 00:28
copumpkinmeaning you're saying it has no computational value, and that nothing that isn't irrelevant can access it18/12 00:28
copumpkin(so it can be ignored at compilation)18/12 00:28
danraha, I see18/12 00:29
danrthank you :)18/12 00:29
Saizanand that values of that record type are considered equal even if they differ at those fields18/12 00:29
danrah, thanks!18/12 00:30
--- Log closed Sun Dec 19 14:36:01 2010
--- Log opened Sun Dec 19 14:36:10 2010
-!- Irssi: #agda: Total of 31 nicks [0 ops, 0 halfops, 0 voices, 31 normal]19/12 14:36
-!- Irssi: Join to #agda was synced in 76 secs19/12 14:37
--- Day changed Mon Dec 20 2010
danrMy agda code takes forever to typecheck... I'm wondering, is it also typechecking the modules imported, or is that cached? (I hope for the latter :) )20/12 12:38
Saizan_cached, it's in the .agdai files20/12 12:41
danrso I hoped20/12 12:42
danrI have some holes in the type signatures, namely what universe level some Sets are going to be in. I'm wondering if that might be what takes so long time20/12 12:42
Saizan_i've read something along those lines from nils20/12 12:44
Saizan_or, at least, that there's some amout of work that's proportional to the number of holes20/12 12:44
Saizan_heavy use of records also tends to be slow20/12 12:46
danrd'oh20/12 12:49
danri have huge records20/12 12:49
Saizan_making some of the fields irrelevant might help, though that's a fairly new/experimental feature20/12 12:53
danryes it's a good idea, though I want to make those fields in a where-clause20/12 12:57
Saizanyou can20/12 12:58
Saizanfoo = record { irr-field = bar } where .bar : _; bar = ...20/12 12:59
Saizan(or maybe you've to put . in front of the third bar too)20/12 12:59
danrhmm i get parse erro when trying to do thot20/12 13:01
danrerror* that*20/12 13:01
danrdo I need the darcs version? I have 2.2.820/12 13:01
Saizanah, i guess so20/12 13:02
danrmaybe time for an update then :)20/12 13:03
roconnoranyone here use PiSigma?20/12 16:00
copumpkinman, you sure are curious about PiSigma :P20/12 16:00
copumpkinI've been tempted to, but haven't needed it just yet20/12 16:00
roconnorPiSigma seems broken to me20/12 16:01
roconnorI figure I must be mistaken20/12 16:01
copumpkinbroken in what way?20/12 16:01
copumpkinnot that I can defend it in any informed way20/12 16:02
copumpkinjust curious20/12 16:02
roconnorit seems impossible to type check expressions with beta-redexes20/12 16:02
roconnorkosmikus: *ping*20/12 16:03
roconnorkosmikus is one of the authors, so maybe he knows.20/12 16:03
roconnorMaybe I can also ask a general question to the channel:20/12 16:07
roconnorWhat type annotations, if any, are needed for dependent pairs in bidirectional type checking?20/12 16:08
Saizanthe last post on e-pig seems to get by with no annotations on the pair constructor20/12 16:42
pigworkerI just published the next post in that series.20/12 16:49
pigworkerNo annotation on pairs. No beta-redexes.20/12 16:49
pigworkerDefinitions are ok, though.20/12 16:50
pigworkerInability to check beta-redexes introduces fewer problems than ability to check beta-redexes, I suspect.20/12 16:51
copumpkinooh20/12 16:54
* pigworker hits the shops20/12 17:06
roconnor?20/12 17:09
roconnoris this related to PiSigma?20/12 17:09
roconnorand aren't beta-redexes important to prevent exponetial blow up in the size of terms20/12 17:09
Saizanpigworker: btw, you say "User-constructed terms contain no β-redexes", but i can imagine writing (\x -> ..) (..) (e.g. desugaring a let), or is this some other sense of user?20/12 17:11
Saizanoh, maybe it's referring only to the types there?20/12 17:12
pigworkerroconnor: you can always hide a beta-redex behind a definition, preserving its typecheckability20/12 19:11
pigworkerSaizan: you can imagine writing (\ x -> ...) (..), but that's a syntax error20/12 19:12
roconnorpigworker: Strange, but okay.20/12 19:12
roconnorpigworker: my real question is about annotations of dependent pairs.  When are they needed?20/12 19:13
roconnorannotations for dependent pairs20/12 19:13
pigworkernot so strange, really; beta-redexes correspond to indirect proofs, which require the statement of the intermediate lemma20/12 19:13
roconnorPiSigma has not annotations of dependent pairs, so type synthesis is not possible.  Unlike for functions, I don't know when you'd want to synthesis types for dependent pairs20/12 19:14
pigworkerit's the same deal for dep pairs, no beta-redexes => no need to annotate pairs20/12 19:14
roconnordo you ever want to do it?20/12 19:14
roconnorwhat do beta-redexes have to do with dependent pairs?20/12 19:15
pigworkerah, I have a more general notion of beta-redex than you, it seems20/12 19:15
roconnorpossibly :)20/12 19:15
pigworkerI think of projection from pairs as beta also20/12 19:16
roconnorso you need synthesis of types for dependent pairs to type check projection of pairs redexes?20/12 19:16
pigworkeryes20/12 19:16
pigworkeronly it's a harder problem than function type synthesis20/12 19:17
roconnorharder really?  Just more sophisticated annotations, no?20/12 19:17
pigworkerI mean, you need more serious annotation more often, because the unaided inference problem is harder20/12 19:18
pigworkerthe tricky bit is figuring out exactly in what way the type of the second component depends on the value of the first20/12 19:20
roconnorindeed20/12 19:21
pigworkerIf you want to do type synthesis (which is basically what you need to check beta-redexes in the general sense), you need pairs like (x=s,t:T) where you can synthesize s:S, then check x:S |- T : Set, before checking that t : T[s/x] and synthesizing (x:S)*T.20/12 19:25
roconnorpigworker: it seems that that nested case and split statements are disallowed (at least in PiSigma) by the typechecking rules.20/12 22:38
roconnore.g.20/12 22:38
roconnorI cannot write "split (split (a,(b,c)) with (x,y) -> y) with (x,y) -> y"20/12 22:39
roconnorsince the argument to split has to a value whose type can be sythensised20/12 22:39
roconnorI can write "split (a,(b,c)) with (x,y) -> split y with (x,y) -> y)" though.  Prehaps the idea is that "programs" must always be written this way.20/12 22:40
roconnorer s/(a,(b,c))/abc20/12 22:41
roconnorwhere abc is some variable with type (A * (B * C)) in the context20/12 22:41
pigworkerroconnor: ah, no motive on case and split, so type synthesis of elimination form impossible?20/12 23:08
pigworkerspecial case of split with variable scrutinee gives easier type synthesis problem20/12 23:11
pigworkerbut of course that's not stable under substitution20/12 23:11
edwinbI was mucking about with pisigma the other day. That does appear to be the case.20/12 23:11
edwinbthe syntax seems to allow it though20/12 23:12
edwinbI obviously read the LambdaPi and PiSigma papers too close together. I was sure I'd read something about bidirectional type checking for PiSigma...20/12 23:21
roconnoredwinb: bidirectional typechecking is section 5 of the PiSigma paper20/12 23:29
roconnorpigworker: I didn't quite understand your comments20/12 23:30
roconnorpigworker: I'm not entirely sure how important it is to be stable under substitution.  After all, once we type check a program we can erase the types, right?20/12 23:31
pigworkerI dunno. I kind of like type preservation as a property.20/12 23:32
roconnorThe wierd thing is that application in PiSigma has type synthesis, but split doesn't.20/12 23:32
roconnorpigworker: didn't you throw out type preservation once you disallowed beta-redexes?20/12 23:33
pigworkersplit is trickier than projections20/12 23:33
edwinboh, clearly I did then20/12 23:33
roconnorpigworker: interesting point about split vs projections.  I was thinking of them as "equivalent"20/12 23:34
roconnorstill without being able to type expressions with beta-redexes, you don't have type preservation?  As soon as I delta-expand definitons I will expose beta-redexes and create a term that won't typecheck.20/12 23:37
pigworkerroconnor: I have big-step type preservation20/12 23:38
roconnorfair20/12 23:38
pigworkerand stability under hereditary substitution20/12 23:38
pigworkerI claim20/12 23:38
* pigworker must do homework20/12 23:38
roconnorsubstitutions don't make beta-redexes?20/12 23:39
roconnoror are the beta-reducing substitutions?20/12 23:39
roconnor*they20/12 23:39
pigworkerhereditary substitution reduces all beta-redexes thus created20/12 23:39
roconnorI see.  But substitution might produce these split-split nested expressions (chi-redexes? xi-redexes?).20/12 23:40
pigworkersure20/12 23:41
roconnorpigworker: epigram 2 has projection functions instead of a split expression and thus avoids this issue?20/12 23:44
pigworkeryep20/12 23:44
roconnorinteresting20/12 23:46
pigworkerstrictly, it has projection for Sigma the way it has application for Pi, a thing that hangs on a spine20/12 23:46
roconnorhow does using projections avoid the type synthesis problem?20/12 23:48
roconnorI would expect the typing rule for projections to be "x => theta, theta ~> simga*tau |- pi1 x <= sigma"20/12 23:49
roconnorbut still the type of x needs to be synthesisable.20/12 23:49
roconnoroh wait, I guess there is a type synthesis rule for projections too20/12 23:49
pigworkeryou don't need to figure out what the projections are *for*, just what they are; the thing you project from must have an inferrable type20/12 23:49
roconnor "x => theta, theta ~> simga*tau |- pi1 x => sigma"20/12 23:50
roconnorI'm starting to see the difference with split20/12 23:50
roconnoris there a problem with a loss of efficency by not having a primitive split operation?  Having to project each and every field out of a tuple to get access to it.20/12 23:52
pigworkeryes, that's the rule20/12 23:52
pigworkerroconnor: I don't know, and I would love to have something working otherwise well enough to care.20/12 23:52
roconnor:)20/12 23:53
edwinbI wouldn't worry about that. Optimisers are quite good at spotting patterns (or being told about them)20/12 23:57
pigworkerIt's quite reasonable to implement split in terms of projection.20/12 23:58
roconnoredwinb: really.  Every time I expect GHC to optimise something obvious, it doesn't.20/12 23:58
pigworkerBy way of pointing out the useful sharing...20/12 23:58
roconnoredwinb: usually I want it to do some sort of CSE and it doesn't20/12 23:58
edwinbthis would be a pretty common pattern for Epigram...20/12 23:58
edwinbCSE is rather harder to do well, iirc20/12 23:59
pigworker"CSE never happens" is an article of faith; I don't mind being proven wrong, here and there.20/12 23:59
--- Day changed Tue Dec 21 2010
edwinbanyway, projection is just adding a number to a pointer, at least the way epic does it21/12 00:00
roconnoredwinb: wow, that sounds really inexpensive21/12 00:04
edwinbit should be21/12 00:05
roconnoredwinb: and kinda strict21/12 00:05
edwinbif you want to split a tuple, you need to have evaluated it...21/12 00:05
edwinbyou don't need to evaluate all the arguments21/12 00:05
edwinbbut you do need to have it in constructor form21/12 00:05
roconnorok21/12 00:06
edwinbGHC only evaluates when it sees a case expression, effectively it'd be the same thing21/12 00:06
roconnorAh, the PiSigma paper says "currently dependent elimintation is only permitted if teh scrutinee is a variable".21/12 01:17
roconnorI guess I should have read it more carefully earlier.21/12 01:17
roconnor"but the current design lacks subject reduction for open terms, so we may reconsider this design choice"21/12 01:19
roconnor"because a variable may get replaced by a neutral term during reduction"21/12 01:20
* roconnor needs to learn what big-step reduction is.21/12 01:20
kamatsuhi, anyone feeling like giving me a hand with getting agda to believe something terminates?21/12 13:14
kamatsuthe algorithm is HM unification21/12 13:14
pigworkerkamatsu: first-order unification (due to Robinson), as used in Hindley-Milner typechecking?21/12 15:02
kamatsupigworker: yeah21/12 15:03
kamatsufor, say, function types (or any application of a type constructor)21/12 15:04
kamatsu(a,b) (c,d) -> unify a and c giving U, unify Ub and Ud giving U', return U u U'21/12 15:04
pigworkeraha, but unifying Ub and Ud ain't structural, right?21/12 15:05
kamatsuyup21/12 15:05
kamatsuthe substitution U means Agda is no longer convinced that it will terminate.21/12 15:06
pigworkerrightly so, as some substitutions might make unification loop21/12 15:06
kamatsuright, but you never get those substitutions in practice21/12 15:06
pigworkerbecause of the occur check21/12 15:07
kamatsuproving termination of unification requires you to prove that.21/12 15:07
pigworkerwhat's your type of terms?21/12 15:10
kamatsuwhat do you mean?21/12 15:11
kamatsuif you mean, what types am i unifying: vars, cons, apps.21/12 15:12
pigworkerthe syntax you're unifying: I guess that's HM types... what datatype do you use to represent it?21/12 15:12
kamatsuapps introduce the recursion.21/12 15:12
kamatsuhttp://hpaste.org/42469/hm_inference21/12 15:12
kamatsuthe right-triangle thing is just substituting on a type21/12 15:14
pigworkerok, although the var ~ some-other-type case is currently missing, but I guess that's on the way21/12 15:15
kamatsuyeah21/12 15:15
pigworkerone thing you can do, to make some progress, is to accumulate the substitution21/12 15:16
kamatsuhm21/12 15:17
pigworkerunify (a,b) (c,d) U0 = unify a c U0 >>= unify b d21/12 15:18
pigworkerpushes the problem to the variables21/12 15:18
kamatsuright21/12 15:18
kamatsualthough i lose my nice notation...21/12 15:18
kamatsuoh wait, agda has mixfix21/12 15:18
pigworkerwhen you hit the variables, you need to apply your accumulated substitution somehow, and that gives you the blowup again21/12 15:21
pigworkeryou can use a variable-counting measure to justify termination, once you prove that the occur check ensures decrease of the variable count21/12 15:24
pigworkerbut I wouldn't recommend it21/12 15:24
kamatsuhm21/12 15:25
kamatsuwhy wouldn't you recommend it?21/12 15:25
pigworkertoo much like hard work21/12 15:25
kamatsuheh21/12 15:26
Saizan_http://code.haskell.org/~Saizan/unification/Unify.agda <- while learning Agda i wrote down that approach (taken from pigworker's paper)21/12 15:26
Saizan_(mgu = most general unifier)21/12 15:26
pigworkerI recommend indexing the syntax by the number of available variables, and writing the occur check with a more informative type.21/12 15:26
kamatsuokay21/12 15:28
kamatsuSaizan_: still got a while to go before I fully understand that, methinks21/12 15:28
kamatsupigworker: is it still advisable to accumulate the unifier? I don't see how it helps21/12 15:30
kamatsuafter all, it just blows up again when you substitute21/12 15:30
kamatsuor is substituting at the same time as the occurs check advisable for some reason?21/12 15:31
pigworkerif you index by number of available variables, each individual substitution maps one of (n+1) variables to a term over the remaining n21/12 15:32
kamatsuright21/12 15:32
kamatsuso, sub : Substitution -> Type (suc n) -> Type n?21/12 15:33
pigworkerif you have one of (n+1) vars and you check if it occurs in a term over (n+1) vars, then either the var occurs, or it's expressible with only n vars, giving you one substitution21/12 15:34
pigworkeryes, each individual variable elimination effectively has that type, and you compute a downward chain of such eliminations21/12 15:35
kamatsuoh, this feels alot like termination checking via transition diagrams that I did at uni21/12 15:36
kamatsufigure out some well-founded order that describes some distance to termination21/12 15:36
pigworkermaybe, but in this case it works out to be a lexicographic structural recursion21/12 15:37
pigworkereach elimination decreases the index, so it doesn't matter if it blows up the terms21/12 15:37
kamatsuso, how does Agda figure that out?21/12 15:37
kamatsuhow does it know to pay attention to the index rather than the terms?21/12 15:38
pigworkerthe termination checker looks for anything which systematically decreases through the call graph of your program21/12 15:38
kamatsui see, okay, i'll give that a go21/12 15:39
kamatsuhm21/12 15:40
kamatsuwait, what if you had a type "Int" and the substitution [x:=Bool]21/12 15:41
pigworkerI did write a paper on this problem (google unification structural recursion) which might help.21/12 15:41
kamatsuor, perhaps more worryingly "y"21/12 15:41
kamatsuy would have 1 variable, but the substitution [x:=Bool] doesn't decrease that.21/12 15:42
kamatsucool, i'll look it up21/12 15:42
Saizan_i guess that's where the "available" helps21/12 15:42
Saizan_you're still producing a term where x is no longer available21/12 15:43
pigworkerthanks Saizan, you type more quickly than I do21/12 15:43
kamatsuso what is the definition of "available" here?21/12 15:45
Saizan_if you parametrize your Term type by the type of variable names, then Term A allows variables from A, and Term B allows variables from B21/12 15:47
pigworkerif you represent variables in Type n as elements of some n-element set Var n, then you have n variables available, but you don't have to use them21/12 15:47
kamatsuright.21/12 15:47
kamatsuhm21/12 15:48
pigworkerindeed, just parametrizing Type by type of vars, then using Type (Var n) would do nicely21/12 15:48
kamatsutype of variables?21/12 15:48
kamatsuright now i'm just representing variables by their name21/12 15:49
kamatsuthey don't have type information until the inferencer figures that out.21/12 15:49
pigworkeryeah, but you could parametrize by the Agda type used to represent names21/12 15:49
kamatsuhm21/12 15:50
kamatsuhow does that help?21/12 15:50
Saizan_because then if you use e.g. Fin (suc n) as the type of variable names you know it has one more variable available than if you used Fin n21/12 15:51
pigworkerthat's the plan: nail down precisely the set of variables in play21/12 15:52
* kamatsu goes to the stdlib to figure out what Fin is21/12 15:52
Saizan_data Fin : Nat -> Set where zero : Fin zero; suc : forall {n} -> Fin n -> Fin (suc n)21/12 15:52
Saizan_i.e. Fin n is a type with n elements21/12 15:52
kamatsubut the type of variable names needs to have unbounded elements because HM inference requires unique names.21/12 15:53
pigworkerhang on, shouldn't that be zero : forall {n} -> Fin (suc n) ?21/12 15:53
Saizan_oh, sure21/12 15:53
pigworkerbut only finitely many names are in use at any one time21/12 15:53
Saizan_data Fin : Nat -> Set where zero : forall {n} -> Fin (suc n); suc : forall {n} -> Fin n -> Fin (suc n) -- sorry21/12 15:53
kamatsuright21/12 15:54
kamatsuso, when constructing a type term, when do i increase this number? whenever i hit a variable?21/12 15:55
kamatsu(x,x) only has 1 variable available21/12 15:55
kamatsuright?21/12 15:55
pigworkerprescription, not description; (x,x) needs at least 1 variable available21/12 15:56
kamatsuso, (x,(x,y)) means that: x needs 2, (x,y) needs 2 ?21/12 15:58
kamatsutrying to figure out how to convert this into agda21/12 15:58
pigworkeryeah, you push the prescription down, rather than trying to bubble a description up21/12 15:59
Saizan_i guess one could aslo use an unindexed Term type, a function usedVars# : Term -> Nat; and then use IndexedTerm n = exists t : Term. usedVars# t <= n21/12 16:02
Saizan_but inductive types are nicer to work with than constrained ones like that, usually21/12 16:02
* kamatsu is indexing his terms now21/12 16:03
roconnorSaizan_: I thought using constraints (such as equality constraints) was all the rage now-a-days for encoding dependent families21/12 16:03
kamatsuah21/12 16:04
kamatsuanother problem21/12 16:04
kamatsui have forall quantors in my term language21/12 16:04
kamatsuhowever they're never touched by unification21/12 16:04
kamatsuwhat should I do with them with regard to indexes?21/12 16:05
kamatsu(i do the  ol' replace every quantified variable with freshies)21/12 16:05
Saizan_roconnor: there's a difference between putting equality constraints inside constructors to encode the refinements and just attach any constraint on top like above, i think, especially if you have tactics that let you work as if you had dependent pattern matching21/12 16:06
pigworkerkamatsu: you might want to keep the forall-bound vars in type schemes conspicuously separate from the free type vars you're trying to solve21/12 16:07
kamatsupigworker: so, in a different type?21/12 16:08
kamatsuquantifiedType and boringType?21/12 16:08
pigworkertype scheme and type21/12 16:08
kamatsuhttp://hpaste.org/42471/type_terms21/12 16:09
kamatsuis this the indexing you meant?21/12 16:09
kamatsuthe arity index is something else, it's ensuring that constructors are all fully applied21/12 16:10
kamatsuyou can ignore that21/12 16:10
kamatsuuh21/12 16:11
kamatsuthat doesn't check at the moment21/12 16:11
kamatsui made a typo21/12 16:11
pigworkereither that, or Type (X : Set) : Arity -> Set, with ... var : X -> Type X 021/12 16:11
pigworkerand then use Type (Fin n) a  for a type with n vars21/12 16:12
kamatsuany benefit of one approach over the other?21/12 16:12
pigworker(\ X -> Type X a) is a monad21/12 16:13
pigworkerwith var as return and simultaneous substitution as bind21/12 16:14
kamatsuah,  nice21/12 16:14
kamatsuthe one thing i don't fully understand is21/12 16:15
kamatsuhow this actually works to give me the number of available variables?21/12 16:16
Saizan_n is that number21/12 16:16
kamatsui understood that much, but if i give it the name "3"21/12 16:16
kamatsua variable, i mean21/12 16:16
kamatsuthen tau-var 3 requires only 1 available variable21/12 16:17
kamatsubut 3 only fits in Fin 3, afaict21/12 16:17
kamatsuhold on, i should probably read the Fin module21/12 16:17
kamatsuokay, i don't understand what this means:21/12 16:19
kamatsu  zero : {n : ℕ} → Fin (suc n)21/12 16:19
pigworkerit's enough that Agda typechecks that you use only variables which are available21/12 16:19
pigworkerFin n has n elements21/12 16:19
pigworkereach nonempty Fin set, i.e., each Fin (suc n) has an element called zero21/12 16:20
kamatsuohh, right21/12 16:20
kamatsuzero is not in Fin 0, right21/12 16:20
kamatsuokay, that makes sense now.21/12 16:21
pigworkerreusing the constructor name from natural numbers, but it ain't the same thing21/12 16:21
kamatsuso it doesn't give you arbitrary range sets21/12 16:21
kamatsuit gives you either empty set or set from 0-n21/12 16:21
pigworkerit's like Fin (suc n) has all the "old" elements of Fin n, embedded by suc, and a "new" one, zero21/12 16:22
pigworkerFin n has representations of numbers from 0 up to n-121/12 16:22
kamatsuright21/12 16:22
kamatsuokay, so i don't see how that gives me a reliable index for the available variables in a type21/12 16:23
kamatsuif i call a type variable "5" then that is only representable in Fin 6, which would imply that that type variable requires 5 variables available when it doesn't.21/12 16:24
kamatsuor is it okay to be over, just not under?21/12 16:25
kamatsu(technically representable in Fin n where n >= 621/12 16:26
pigworkerif you have only one variable available, it is the zero of Fin 121/12 16:26
pigworkerand yes, there's a 5 in Fin at-least-621/12 16:27
kamatsuthat's the part i don't understand.21/12 16:28
pigworkerAgda will bound-check all the variables you use in a term, and if you're lucky, it'll infer a lower bound21/12 16:28
kamatsuso, if i end up with the term (x,(x,y)) how does it figure out that that has 2 available variables?21/12 16:29
kamatsuor, well, the variable names are actually elements of fin, so (1,(1,2))21/12 16:29
kamatsuwouldn't it say 2 fits in Fin 3, so it requires 3 variables, therefore the rest require 3 variables?21/12 16:30
kamatsubut it only requires 2.21/12 16:30
pigworkerwhat it requires is not important21/12 16:31
pigworkeryou have used 1 and 2, 0 is available, even if you don't use it21/12 16:31
kamatsuokay21/12 16:31
kamatsui see.21/12 16:31
kamatsunow, if I have a substitution, [4 := blah ]21/12 16:33
kamatsuand i try to apply it to that term, it won't do anything because it isn't dealing with an available variable, right?21/12 16:33
kamatsubut if i had [0 := blah] that will reduce the amount of available variables, although the term remains unchanged21/12 16:34
pigworkeryou need to make sure the type of substitutions fixes its domain to be the set of available variables21/12 16:35
kamatsuhm, so, in terms of code, should I represent my substitutions as a function from Fin n to Fin (n-1)?21/12 16:36
kamatsuor, Type (Fin n) to Type (Fin n-1)21/12 16:36
kamatsui mean21/12 16:36
kamatsu(rearranging with sucs and such)21/12 16:36
pigworkersubtraction often best avoided21/12 16:37
kamatsuyeah21/12 16:37
kamatsuso, Type (Fin (suc n) -> Type (Fin n)21/12 16:37
kamatsumissed a bracket21/12 16:37
Saizan_Fin (suc n) -> Type (Fin n) actually, which you transform into Type (Fin (suc n)) -> Type (Fin n) with the (=<<) of the Type monad21/12 16:38
kamatsuoh, right21/12 16:38
kamatsuyes21/12 16:38
pigworkerthat's how it's used, but I might like to represent it more concretely as a pair (Fin (suc n), Type (Fin n)), then apply it as Saizan suggests21/12 16:38
kamatsuright, i currently have it as a pair so that wouldn't be difficult to change21/12 16:38
kamatsudoes that mean that applying the substitution (0:=blah) to (1,1) would give me a new term (0,0) ?21/12 16:39
kamatsuoh wait21/12 16:40
kamatsuyou have to apply the highest substitution first?21/12 16:40
kamatsuah, so in that case it makes sense to accumulate the substitutions so that you can apply them in some semblance of order.21/12 16:40
pigworkerwhen you apply a substitution (i, t), all the variables above i get decremented21/12 16:41
kamatsuso if i have several substitutions21/12 16:42
pigworkerand your accumulator is a chain of substitutions, stepping down one at a time21/12 16:42
kamatsudoes that mean i must decrement every subsequent substitution as well?21/12 16:42
kamatsuthe variable names that occur in them i mean.21/12 16:42
kamatsuotherwise if i had [ 0:=foo, 1:=bar] for (0,1) then i'd end up with (foo,0) and then i'd have to change 1:=bar to 0:=bar21/12 16:43
kamatsuor will my substitution chain always be in the order [1:=bar, 0:=foo] thus avoiding that issue.21/12 16:44
pigworkerit could be [ 0:= foo, 0:=bar ]21/12 16:44
kamatsuhm21/12 16:45
pigworkerafter 0 := foo, the old 0 is gone and the old 1 is the new 021/12 16:45
kamatsuright, but how does the unification algorithm produce such a substitution21/12 16:45
kamatsuit would see the term (0,1) and the term (foo, bar)21/12 16:46
kamatsuunify 0 and foo giving 0 := foo21/12 16:46
kamatsuoh21/12 16:46
kamatsuand then it would unify 0 and bar..21/12 16:46
Saizan_the AList type in the Unify.agda i linked above makes sure each singular susbtition works on the variables left by the previous, and it seems to work well as an accumulator for the unification algorithm21/12 16:46
Saizan_(though i've never tried to implement HM out of that)21/12 16:47
kamatsui'm actually having fun implementing HM in data constructors21/12 16:48
kamatsui'm going to try and make it impossible to construct a incorrectly typed term.21/12 16:48
kamatsuokay, so if i just make substitutions perform that decrementing as well as the substitution21/12 16:49
kamatsuwill everything work out?21/12 16:50
kamatsuor is there anything else I should be aware of21/12 16:50
kamatsuthen the next puzzle is the occurs check but i'll do that after I've finished the rest of unification21/12 16:50
pigworkerI don't know how easily HM will work out, but unification should be ok.21/12 16:51
kamatsupigworker: well, assuming a working unification algorithm, i can infer basic types, and I've threaded through some fresh name source that should help the rest of it21/12 16:51
pigworkerWhen you hit a variable, you can apply the topmost elimination in your accumulator, and that decrements the index.21/12 16:52
pigworkerWhen you generate fresh vars, that means shifting to work over Type (Fin (m + n)), which may take some care, but should work.21/12 16:54
kamatsu4hm21/12 16:55
kamatsuI didn't realise until just now that using this naming scheme will make name generation more difficult21/12 16:55
kamatsuis there a simple way to get equality of two Fin n's ?21/12 17:02
kamatsuas a Bool21/12 17:02
kamatsui want to determine if two names are the same21/12 17:07
kamatsuit seems like Agda only makes that easy with strings, I think i'm missing something21/12 17:07
kamatsu> agdagle Fin n -> Fin n -> Bool21/12 17:11
lambdabot  <no location info>: parse error on input `->'21/12 17:11
kamatsui gues no one has written a hoogle counterpart for agda21/12 17:11
kamatsu*guess21/12 17:11
Saizan_heh, no21/12 17:13
kamatsuoh well, i suppose it's not too hard to write one.. zero == zero, suc n == suc m if n == m.21/12 17:13
Saizan_right21/12 17:13
Saizan_see my ≡Fin if you want something better than Bool21/12 17:14
kamatsuI saw that in the standard libraries before21/12 17:15
kamatsuwhat makes it better than bool? use in proofs?21/12 17:15
kamatsuah, it's accompanied by a proof it seems21/12 17:16
Saizan_yep21/12 17:21
Saizan_the result if far more meaningful, since it contains a proof of (in)equality21/12 17:21
kamatsuis there an easy way to go from such a result to a bool? just because I use it in a filter function on a list21/12 17:22
kamatsuor is there a better way to do that too?21/12 17:22
kamatsuI saw some of that Any/All stuff with lists but i didn't make a whole lot of sense of it21/12 17:22
Saizan_toBool (yes _) = true; toBool (no _) = false; -- not sure if it's in the stdlib21/12 17:24
kamatsuright21/12 17:25
Saizan_a term of type "All P xs" is a proof that all the elements of xs satisfy the predicate P, which is represented essentially by a list of P x, where x is one such element of xs21/12 17:26
Saizan_Any P xs means there's at least one element of xs that satisfies P, and it's represented by an index which tells us which element it is, and the corresponding proof that it satisfies P21/12 17:27
kamatsui see21/12 17:32
kamatsuthanks21/12 17:32
kamatsuokay, so am i right in saying that my chain of substitutions will have varying indices and so the type of the container should be something like21/12 17:33
kamatsuList (all n. Fin (suc n), Type (Fin n))21/12 17:34
kamatsuor does the all n go on the outside?21/12 17:34
kamatsu(where , is times and all is forall21/12 17:34
Saizan_if you want each element to be able to decide its own n you should use exists instead of all21/12 17:35
pigworkerif you want to be able to apply the chain of substitutions in sequence, you might want to be more precise21/12 17:36
Saizan_yeah21/12 17:36
kamatsuhm21/12 17:37
Saizan_data AList : ℕ -> ℕ -> Set where anil : ∀ {n} -> AList n n _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m)) -> AList (suc m) n21/12 17:38
pigworkerwhich is a special case of reflexive-transitive closure21/12 17:39
Saizan_a term of type AList m n, is a chain of substitutions that as a whole map terms with m available variables to terms with n available parameters21/12 17:40
kamatsuparameters? you mean variables?21/12 17:40
Saizan_yes, sorry :)21/12 17:40
kamatsuSaizan_: your AList looks good, i'll shamelessly steal it21/12 17:56
Saizan_kamatsu: heh, i did the same at the time :)21/12 17:59
kamatsuhm21/12 18:04
kamatsuwith the unification, are the indices of both types the same? not necessarily, right?21/12 18:05
pigworkeryes necessarily21/12 18:05
kamatsuright21/12 18:05
kamatsuso just say so in your type sig?21/12 18:05
pigworkeryeah21/12 18:06
pigworkerI mean, you expect unification problems to agree on the names of the variables involved21/12 18:06
kamatsuright21/12 18:08
kamatsuunify: ∀ {n a} → Type (Fin n) a → Type (Fin n) a → Unifier → Maybe Unifier21/12 18:08
kamatsuwhere Unifier is Saizan's AList21/12 18:08
kamatsuthe first one is the accumulator21/12 18:09
kamatsunow, what are the two indices i give it?21/12 18:09
pigworkeryou'll probably need that your Unifiers start at index n21/12 18:09
kamatsuand map to.. some m?21/12 18:09
pigworkerto some existentially quantified m -- you can't predict it up front21/12 18:10
kamatsuhow's this -- unify: exists p q -> ∀ {n a} → Type (Fin n) a → Type (Fin n) a → Unifier n p → Maybe (Unifier n q)21/12 18:10
kamatsuaccum and result would have to map to different variables right? because the accum starts off mapping to n.21/12 18:11
kamatsubut that doesn't state anywhhere that p, q <= n21/12 18:12
Saizan_you want to push the exists down21/12 18:13
kamatsuhm, so:21/12 18:13
Saizan_∀ {n a} → Type (Fin n) a → Type (Fin n) a → (exists p. Unifier n p) → Maybe (exists q. Unifier n q)21/12 18:13
kamatsuright21/12 18:14
Saizan_otherwise you've to choose them before you've looked at the terms21/12 18:14
kamatsuah, i see.21/12 18:14
Saizan_and p is actually given to you21/12 18:14
kamatsuhow so?21/12 18:14
Saizan_(exists p. Unifier n p) is like a tuple of a natural p and an Unifier n p21/12 18:15
kamatsuoh right, the witness to the existential21/12 18:16
Saizan_also, you can deduce p <= n by Unifier n p21/12 18:17
kamatsuah21/12 18:17
kamatsu _∼_accum_ : ∀ {n a} → Type (Fin n) a → Type (Fin n) a → (∃ (Unifier n)) → (Maybe ( ∃ (Unifier n)))21/12 18:19
kamatsucorrect?21/12 18:19
Saizan_yep21/12 18:20
kamatsuhttp://hpaste.org/42476/unifier21/12 18:22
kamatsuthis is wrong21/12 18:22
kamatsui know it is21/12 18:22
kamatsubut just posting it for reference21/12 18:22
kamatsuso i'm figuring out what to do in the var/var case.21/12 18:22
kamatsui imagine i have to perform substitution at that point?21/12 18:23
kamatsu(also i know the var/other case still isn't there)21/12 18:23
pigworkeryou'll need to start examining the accumulator, substituting for the vars21/12 18:24
pigworkerif the accumulator is empty, you can start solving for variables!21/12 18:25
kamatsuso do you just apply every single substitution in the accumulator and then go?21/12 18:26
pigworkerone at a time is easier21/12 18:26
kamatsuright, but continue until all gone?21/12 18:26
kamatsuthen generate new substitutions, return that substitution in addition to all the substitutions you just applied?21/12 18:27
pigworkeryep21/12 18:27
kamatsuokay, doesn't sound hard21/12 18:27
kamatsuwhat could possiblai go wrong21/12 18:27
kamatsuthis only applies if the variables are different right?21/12 18:28
kamatsuif they're the same you just bail out21/12 18:28
kamatsureturn the accumulator21/12 18:28
kamatsuor do you apply the substitutions even if they are the same?21/12 18:29
kamatsuhm21/12 18:30
kamatsuactually, it occurred to me that substitution could cause them to no longer be the same.21/12 18:30
kamatsuas in, not even var/var anymore21/12 18:30
kamatsuso i suppose i should tackle the var/any case21/12 18:30
kamatsuwhere var/var is essentially a special case of that21/12 18:30
kamatsuhm21/12 18:31
kamatsuwait21/12 18:31
kamatsui think i see what pigworker was saying now21/12 18:31
kamatsujust apply one substitution, unify again21/12 18:31
kamatsuand if the accumulator is empty then start checking stuff because then you have no substitutions21/12 18:32
pigworkerexactly21/12 18:32
kamatsu  (τ-var x  ) ∼ (τ-var y   ) accum (v , empty) with x ≡Fin y21/12 18:34
kamatsu  ...                                | yes _ = just (v , empty)21/12 18:34
kamatsuwith the no case, what value do i provide as a witness?21/12 18:35
kamatsupred v?21/12 18:35
kamatsuoh wait21/12 18:37
kamatsuit's probably pred n right?21/12 18:37
kamatsuwe've got a Type (Fin n) we end up producing a substitution that goes to Type (Fin (pred n)), which is the only substitution in the list21/12 18:38
pigworkeryou could put _ and see if Agda guesses the witness21/12 18:38
kamatsunot really sure what this error message means21/12 18:40
kamatsuhere's my no case21/12 18:40
kamatsu  ...                                | no _  = ( _ , [ x ≔ (τ-var y)]∷ empty)21/12 18:40
kamatsuv != suc (_192 v x y .¬p) of type ℕ21/12 18:40
kamatsuwhen checking that the expression x has type21/12 18:40
kamatsuFin (suc (_192 v x y .¬p))21/12 18:40
kamatsui think it's saying that the index it got from my type isn't right.21/12 18:41
kamatsuit highlights the x.21/12 18:41
pigworkeryou might need to make sure x isn't in Fin zero21/12 18:42
kamatsubut that's impossible.21/12 18:43
kamatsuFin zero contains no elements21/12 18:43
kamatsushould i just put suc around all my n's?21/12 18:43
pigworkeryou may need to remind Agda of this fact21/12 18:44
pigworkerwherever you have a variable, you can split n into zero and suc, then get rid of the zero case by putting the absurd pattern () for the impossible variable21/12 18:45
kamatsuis there a way to match on implicit parameters while using mixfix syntax in your pattern?21/12 18:46
kamatsuor do i have to use _'s everywhere21/12 18:47
kamatsuhm21/12 18:49
kamatsuthis is getting syntactically messy21/12 18:49
kamatsuoh wait21/12 18:49
kamatsu(nevermind)21/12 18:50
kamatsuhm21/12 18:50
kamatsubut if n cannot be zero21/12 18:50
kamatsuthen it complains about the accumulator21/12 18:51
kamatsusuc n != v of type ℕ21/12 18:51
kamatsuwhen checking that the pattern empty has type Unifier (suc n) v21/12 18:51
kamatsuwhere v is just the  witness21/12 18:53
kamatsufor the accumulator21/12 18:53
pigworkeryou might need a .pattern21/12 18:53
pigworkeror you could use the witness as the thing you match on21/12 18:54
kamatsupigworker: how so?21/12 18:56
pigworkerwell, when the acc is empty, your witness must be the same as n21/12 18:56
pigworkerI mean, the same as the number of variables you started with21/12 18:57
pigworkerso you could split that into zero and suc cases21/12 18:57
kamatsu  _∼_accum_ (τ-var x  )  (τ-var y   ) (suc n , empty) with x ≡Fin y21/12 18:58
kamatsu  ...                                | yes _ = just (suc n , empty)21/12 18:58
kamatsu  ...                                | no _  = (  n , [ x ≔ (τ-var y)]∷ empty)21/12 18:58
kamatsunow it complains about the empty at the end of the final line21/12 18:59
kamatsun != suc n21/12 18:59
pigworkeryeah, your no case also needs to give suc n as the witness for the output21/12 19:00
kamatsureally?21/12 19:01
pigworkerno, I'm being dim21/12 19:01
kamatsui actually get an identical error21/12 19:01
kamatsubut yeah, larger unifier -> smaller witness21/12 19:01
pigworkeryou get down from suc n to n in this move, right?21/12 19:01
kamatsusure, you perform one substitution21/12 19:01
pigworkernow, I can see that tau-var y is of the wrong type21/12 19:02
kamatsuah21/12 19:02
pigworkerrather than knowing that y isn't x, you need to know what it becomes after you eliminate x21/12 19:03
kamatsuso we decrement it?21/12 19:04
kamatsuiff y > x ?21/12 19:04
pigworkeryes, you can replace =Fin with an operation which tries to do that, and fails if y is x21/12 19:05
pigworkerthe point of testing is to acquire useful information21/12 19:05
kamatsuwhat if y is zero21/12 19:05
kamatsu?21/12 19:06
pigworkerthen it isn't bigger than x21/12 19:06
kamatsuoh, right21/12 19:06
kamatsuso, the operation is "compare x y, if >, y-1, <, y, ==, fail" ?21/12 19:08
* kamatsu probably should use more variety in my punctuation21/12 19:08
pigworkeryes21/12 19:09
pigworkersomething with type   forall {n} -> (x y : Fin (suc n)) -> Maybe (Fin n)21/12 19:10
kamatsutrying to use compare, but it doesn't seem to work as i'd like21/12 19:15
kamatsu  foo : ∀ {n} → (x y : Fin (suc n)) -> Maybe (Fin n)21/12 19:19
kamatsu  foo x y with compare x y21/12 19:19
kamatsu  ...           | equal _     = nothing21/12 19:19
kamatsu  ...           | greater _ _ = just (p x)21/12 19:19
kamatsu  ...           | less _ _    = just x21/12 19:19
kamatsui != x of type Fin (suc n)21/12 19:19
kamatsuwhen checking that the pattern equal _ has type21/12 19:19
kamatsuData.Fin.Ordering x y21/12 19:19
pigworkeryour x coming out is still in the big set21/12 19:21
kamatsuah, right, but it fits in the smaller set too21/12 19:22
kamatsuso i need to change the type somehow21/12 19:22
pigworkerits type doesn't reveal that21/12 19:22
kamatsuthat's why i compare to find out.21/12 19:22
kamatsuhm21/12 19:22
kamatsuthat's not the right way to do it then21/12 19:23
pigworkeryour foo is fairly easy to define by recursion21/12 19:23
kamatsuokay, i'll try it that way21/12 19:23
kamatsu  foo : ∀ {n} → (x y : Fin (suc n)) → Maybe (Fin n)21/12 19:29
kamatsu  foo (suc m) (suc n) with foo m n21/12 19:29
kamatsu  ...     | nothing = nothing21/12 19:30
kamatsu  ...     | just v = just (suc v)21/12 19:30
kamatsu  foo (suc m) zero = just m21/12 19:30
kamatsu  foo zero n = just n21/12 19:30
kamatsucomplains that m is in the wrong set on the second line21/12 19:30
kamatsu.n != (suc (_126 m n)) of type ℕ21/12 19:30
kamatsuoh, forgot the zero zero case, but the error is the same21/12 19:32
pigworkerin line 2, you need to make sure m and n are not in Fin zero21/12 19:35
pigworkersplit the index and kill the impossible case again21/12 19:36
kamatsuokay, but now it's complaining about the zero/n case21/12 19:37
kamatsusuc .n != .n21/12 19:38
kamatsui think it thinks it's in the bigger set again21/12 19:38
pigworkeryou need to treat zero zero and zero suc differently anyway21/12 19:38
kamatsuyeah, i added that21/12 19:38
kamatsuzero zero -> nothing21/12 19:38
kamatsusuc n zero -> n21/12 19:39
kamatsuzero n -> n21/12 19:39
kamatsuproblem is that zero n -> n doesn't work..21/12 19:39
pigworkerare you sure (suc m) zero gives just m ?21/12 19:41
kamatsuoh wait21/12 19:41
kamatsuit should give zero21/12 19:42
kamatsunot n21/12 19:42
kamatsuzero n -> zero21/12 19:42
kamatsubut then it goes crazy with "number of arguments in the equations differ"21/12 19:43
kamatsuwhen they don't afaict21/12 19:43
pigworker(..)?21/12 19:46
kamatsuhold on21/12 19:46
kamatsui screwed this up21/12 19:46
kamatsuhm21/12 19:50
kamatsui'm really confused now21/12 19:50
kamatsuwhat does the error "The number of arguments in the defining equations differ" mean exactly?21/12 19:50
kamatsuoh wait21/12 19:52
kamatsusorted it out21/12 19:52
kamatsuokay, i got it to check but it doesn't do the subtraction21/12 19:56
kamatsuok21/12 19:59
kamatsuhm21/12 19:59
kamatsuokay, got it21/12 20:01
kamatsusorry about that21/12 20:01
kamatsuokay21/12 20:59
kamatsuit applies the substitution okay21/12 20:59
kamatsuand also then solves for more substitutions after21/12 20:59
kamatsunow i'm up to the occurs check21/12 20:59
copumpkinkamatsu: whatcha writing?21/12 21:01
kamatsucopumpkin: hindley milner type inference21/12 21:01
copumpkinoh nice21/12 21:01
kamatsuran into a problem with unification - it doesn't terminate21/12 21:02
kamatsuobviously21/12 21:02
copumpkinin agda, it doesn't terminate? :O21/12 21:02
kamatsui mean21/12 21:02
kamatsuit doesn't obviously termiante21/12 21:02
copumpkinoh ok :)21/12 21:02
kamatsuanyway, pigworker and Saizan_ were helping me by showing their prior work in the area21/12 21:02
kamatsubut my overall goal is to make a set of language terms where the W algorithm is encoded into their data structures so that you can't construct a term unlesss it is well typed21/12 21:03
kamatsu*data constructors21/12 21:04
kamatsuso I'm thinking: occurs : Fin (suc n) ->  Type (Fin (suc n)) -> Maybe (Type (Fin n))21/12 21:06
kamatsuand it will handle the decrement as well21/12 21:06
copumpkinwhat's the index on the Type ?21/12 21:09
kamatsuthe type of the typenames.21/12 21:11
kamatsuso, the type of the names you can give to type variables21/12 21:11
kamatsuas we can show that substitution reduces the set of available names used by a type term21/12 21:12
kamatsuif we use a finite set of numbers as your set of available names, Agda can see that the available names set is decreasing and therefore determine that unification terminates21/12 21:13
kamatsuhence the Fin21/12 21:13
kamatsu*used is a wrong word21/12 21:13
kamatsutype terms don't necessarily have to use every name in the set21/12 21:14
copumpkinkamatsu: ah, I see21/12 22:36
--- Day changed Wed Dec 22 2010
kamatsuSaizan_: pigworker: if you're still here, i'm trying to work out how i might have a union of two of Saizan's ALists/my unifiers.22/12 08:54
kamatsuin particular, what happens to the indices22/12 08:55
kamatsushould I only have to do Unifier m n -> Unifier n o -> Unifier m o22/12 08:56
Saizan_kamatsu: yeah22/12 08:59
Saizan_i've them the other way around in my code _++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n, but it doesn't really matter22/12 09:01
kamatsuSaizan_: ah, right22/12 10:18
kamatsuis there a way to "unwrap" an existential?22/12 10:32
kamatsubecause my unifier returns exists ( unifier n)22/12 10:33
kamatsuand so therefore applying that unifier to a type has to return exists n. (type (fin n)22/12 10:33
kamatsuand then trying to unify that resultant type means that I need to unwrap the existential because unify doesn't take existentials as arguments22/12 10:34
kamatsui'm probably just missing something obvious because i'm tired..22/12 10:35
kamatsualternatively, a way to lift unify easily into an existential would also work22/12 10:36
Saizan_kamatsu: you can pattern match on it like an haskell tuple22/12 10:50
Saizan_kamatsu: or use proj\_222/12 10:50
kamatsuah, right22/12 10:59
kamatsucould i write a function: exists (unifier m) -> unifier m n?22/12 11:00
kamatsui guess not22/12 11:00
kamatsui need to learn some first order logic22/12 11:00
Saizan_(u : ∃ (Unifier m)) -> Unifier m (proj₁ u)22/12 11:01
Saizan_that one you can write22/12 11:02
kamatsuah, that's what I was after22/12 11:02
Saizan_it's proj\_2 with a restricted type22/12 11:03
kamatsuoh, right.22/12 11:04
kamatsuannot instantiate the metavariable _538 to proj₁ T₁ since it22/12 11:06
kamatsucontains the variable T₁ which _538 cannot depend on22/12 11:06
kamatsuhm22/12 11:06
kamatsuyou can't pattern match in lambdas?22/12 11:26
kamatsu>_>22/12 11:26
kamatsu\ ( x , y , z ) -> blah doesn't work22/12 11:26
Saizan_no, you can't :\22/12 11:27
kamatsuany way to do pattern matching without writing another binding?22/12 11:27
Saizan_no22/12 11:27
kamatsudrat22/12 11:27
kamatsufor those that have been following, i've encountered another problem that I don't know how to fix22/12 13:17
kamatsuhttp://hpaste.org/42488/problems_again22/12 13:17
kamatsu(aware i could be using state monad for unique names, decided not to worry about it for now)22/12 13:17
kamatsugives me a funny error on the last line that I don't understand22/12 13:17
kamatsuCannot instantiate the metavariable _609 to x since it contains the22/12 13:18
kamatsuvariable x which _609 cannot depend on22/12 13:18
danrkamatsu: did you solve you problem?22/12 16:11
kamatsudanr: nope22/12 16:26
kamatsutook a break for a while22/12 16:26
danrI'm not sure what the problem is, but it seems T1 depends on n22/12 16:34
danrmaybe you want to move the forall n to after SimpleExpr in the type signature22/12 16:35
danror even return the n in the Maybe?22/12 16:35
danr(just some ideas)22/12 16:35
danror is n guaranteed to be the same in the entire run of infer?22/12 16:36
kamatsudanr: so I tried changing it to use an existential, i.e there exists an n22/12 16:46
kamatsudoesn't seem to make a difference22/12 16:46
kamatsu  Environment String → UniqueNames → SimpleExp → Maybe (∃ (λ n →(Type (Fin n) × (∃ (Unifier n)) × UniqueNames)))22/12 16:46
kamatsuexactly  the sameerror so I'm not sure what I'm doing wrong22/12 16:47
danrI don't know of a way to get more information out of that error message22/12 16:47
danrare you sure if T1 or ▹ contains the variable?22/12 16:48
kamatsuwhich variable?22/12 16:59
kamatsuthe funny thing is there is no variable x there.22/12 17:00
jeltschHi, I have a problem with running the Agda emacs mode under Ubuntu maverick.22/12 20:24
jeltschI installed the Ubuntu package agda-mode.22/12 20:24
jeltschHowever, I also installed other Haskell packages (unrelated to Agda) via cabal-install as an ordinary user.22/12 20:25
jeltschSurprisingly, cabal-install installed me another instance of haskeline-, although there already had been a system-wide haskeline- installed as a dependency of the agda-mode package.22/12 20:26
jeltschNow, GHCi wants to load the user-installed haskeline and complains that the hash is wrong.22/12 20:27
jeltschI get this in the *ghci* buffer:22/12 20:27
jeltschPrelude> :set -package Agda-2.2.622/12 20:27
jeltschcannot satisfy -package Agda-2.2.6:22/12 20:27
jeltsch    Agda-2.2.6-6853bd28846ffbb61eaa62b6ffc7dafa is unusable due to missing or recursive dependencies:22/12 20:27
jeltsch      haskeline- 20:27
jeltschAny idea how to resolve this?22/12 20:28
Saizanjeltsch: ghc-pkg unregister --user --force haskeline- 20:30
jeltschSaizan: But this will make all packages that depend on the user-installed haskeline unusable, wouldn’t it?22/12 20:31
Saizanjeltsch: yep22/12 20:31
jeltschBy the way, do you know why cabal-install installed this second instance of haskeline at all? I thought that it should just use the system-wide instance.22/12 20:32
Saizanthe likely cause is that you installed a later version of some lib haskeline depends on, so when cabal-install tried to figure out which libs to use, it committed to that later version and so couldn't use the system-wide haskeline anymore22/12 20:34
jeltschSaizan:22/12 20:38
jeltschSaizan: So you mean, it installed the same version of haskeline that, however, used a different version of another library?22/12 20:39
Saizanyep22/12 20:39
jeltschHmm.22/12 20:39
Saizanyou can check with ghc-pkg field haskeline depends22/12 20:40
jeltschAt the moment, unregistering haskeline isn’t that problematic, since only the darcs library depends on it, and I only need the darcs executable.22/12 20:40
jeltschBut the same problem could occur later if some other software needs haskeline.22/12 20:40
jeltschCan I tell GHCi to ignore all user-installed packages? The system-wide Agda package doesn’t use any user-installed packages, of course.22/12 20:42
Saizantwo installations of the same version of haskeline are very likely to confuse cabal in the future22/12 20:43
Saizani'm not sure if there's a flag to make ghci ignore the user installed packages, you could pass it -package-id Agda-2.2.6-6853bd28846ffbb61eaa62b6ffc7dafa though22/12 20:44
jeltschSaizan: Ah, this seems to work!22/12 20:46
jeltschCan I make the emacs mode to use this flag instead of -package Agda-2.2.6?22/12 20:46
Saizani don't know22/12 20:47
jeltschSaizan: I just found out that there is the option -no-user-package-conf for GHC, by the way.22/12 20:55
jeltschSaizan: And now I found out that in the agda2 group of the emacs configuration there is an entry “Agda2 Ghci options”. :-)22/12 21:21
Saizangreat :)22/12 21:22
jeltschWell, -no-user-package-conf doesn’t seem to have any effect when done using :set inside GHCi (which is what Agda does).22/12 21:22
jeltschHowever, your trick with -package-id Agda-2.2.6-6853bd28846ffbb61eaa62b6ffc7dafa worked. :-)22/12 21:23
jeltschSaizan: Thanks a lot.22/12 21:23
Saizannp22/12 21:23
Saizani'm a bit surprised that -package-id Agda-2.2.6-.. works with :set22/12 21:24
jeltschWell, -package Agda-2.2.6 works too. (This is what Agda does normally.)22/12 21:24
Saizanyeah, but -package-id is supposed to affect the database of packages ghci sees in the current session, i thought that got fixed at the start, fortunately it seems it isn't :)22/12 21:27
--- Day changed Sun Dec 26 2010
rodrigoHello all!26/12 22:08
lispy_hey26/12 22:08
rodrigoI'm starting to learn agda reading Dependently typed programming in Agda by Ulf Norell26/12 22:09
rodrigowhen I got stuck on a example of this article26/12 22:09
rodrigoCan someone help me with this?26/12 22:09
rodrigothe example is the function lookup that does a safe list lookup ...26/12 22:10
copumpkinprobably, but it's hard to say until you ask the actual question :)26/12 22:11
rodrigoI've typed the code of this function exactly as the paper26/12 22:11
rodrigobut when I tried to load the code on emacs26/12 22:11
rodrigoI've got an error message saying that the expression p, in the last equation, doesn't have the type isTrue (n < length xs)26/12 22:12
rodrigohere is the code26/12 22:12
rodrigolookup : {A : Set}(xs : List A)(n : Nat) -> isTrue (n < length xs) -> A26/12 22:12
rodrigolookup [] n ()26/12 22:12
rodrigolookup (y :: ys) zero p = y26/12 22:12
rodrigolookup (y :: ys) (succ n) p = lookup ys n p26/12 22:13
copumpkinwhat type does it have?26/12 22:15
rodrigothe function lookup has the following type26/12 22:15
rodrigolookup : {A : Set} (xs : List A)(n : Nat) -> isTrue (n < length xs) -> A26/12 22:16
copumpkinyeah, I can see that :P26/12 22:16
copumpkinI'd just like the actual error message26/12 22:16
rodrigosorry... rs26/12 22:16
rodrigothe problem26/12 22:16
rodrigois that the agda insists that has an error on the "p" on the right hand side of the last equation26/12 22:17
copumpkinso replace the p with a question mark26/12 22:17
rodrigosaying that n != (length ys) of type Nat26/12 22:17
copumpkinand then load the file26/12 22:17
rodrigook26/12 22:17
rodrigowhat's the meaning of a question mark?26/12 22:18
copumpkinthen then C-c C-,26/12 22:18
rodrigoit will be inferred?26/12 22:18
copumpkinit puts a hole in26/12 22:18
copumpkinnah26/12 22:18
rodrigoit worked!26/12 22:18
rodrigothank you!26/12 22:18
copumpkinwell, that's not enough26/12 22:19
copumpkinthe hole is something you need to fill eventually26/12 22:19
copumpkinbut if you do C-c C-, in the hole, it'll tell you what it wants there and what you have26/12 22:19
--- Day changed Tue Dec 28 2010
kamatsuhey, when I try and unwrap an existential (using uncurry)28/12 05:40
kamatsuit tells me:28/12 05:40
kamatsuCannot instantiate the metavariable _652 to Unifier (_650 Γ δ a b c28/12 05:40
kamatsuτ₁ T₁ δ₁ τ₂ T₂ δ₂) x since it contains the variable x which _65228/12 05:40
kamatsucannot depend on28/12 05:40
kamatsuwhat does this message mean?28/12 05:41
liyangkamatsu!28/12 05:58
liyanghttps://github.com/liamoc/learn-you-an-agda/raw/master/illustrations/completed/cover.png is awesome. Just sayin'.28/12 05:59
kamatsuliyang: thank you, but it was my gf who did it, not me28/12 06:50
djahandarieNeat, that is getting done?28/12 06:51
* djahandarie recalls seeing a tweet28/12 06:51
kamatsudjahandarie: yes, i'm slowly writing it28/12 06:52
kamatsubut i fear my experience is too limited, so i'm doing my best to learn more agda as well as write about the stuff i already understand well28/12 06:52
kamatsui understand quite alot but i don't feel like an expert28/12 06:53
djahandarieI'd proofread for you, but I'm even worse at Agda than you are so I wouldn't be of any help. ;)28/12 06:55
kamatsuI think it's probably a good approach to just write what I understand, clean it up into book form28/12 06:56
kamatsuand then write new chapters as I learn and digest new stuff28/12 06:56
kamatsuTacticalGrace taught me the basics, the rest I learnt by myself and from Ulf's tutorial. There really is a lack of good resources for agda learning.28/12 07:00
djahandarieMan, reading the standard library right now and Algebra.agda sure feels a lot nicer than what Haskell provides28/12 07:02
liyangkamatsu: I'd be happy to read over stuff too.28/12 07:08
kamatsucool, thanks28/12 07:12
kamatsucopumpkin suggested a type-safe printf as a worked example28/12 07:13
kamatsui've implemented one, seems like a good example28/12 07:13
kamatsudoesn't require too much complicated stuff and introduces alot of concepts28/12 07:13
kamatsuhttps://github.com/liamoc/learn-you-an-agda/raw/master/Printf.agda28/12 07:16
kamatsuoh, it just occurred to me that the impossible case can probably just use an absurd pattern ()28/12 07:20
kamatsui'll fix that28/12 07:20
kamatsuah, actually, it can't28/12 07:22
kamatsunevermind28/12 07:22
kamatsui think I know what I'll do for my phd, when i get there28/12 09:01
kamatsui want to create a special Owicki Gries monad, that internally wraps around Haskell IO28/12 09:02
kamatsubut keeps track of the shared variables accessed in the program28/12 09:02
kamatsuthen it should be possible to generate a transition diagram automatically from that monad28/12 09:02
kamatsuand perform verification of shared-variable concurrent programs on those diagrams.28/12 09:02
sullyhm; "Dependently Typed Programming in Agda" mentions the "summer school library" a bunch but never mentions where that lives28/12 23:40
sullydoes anybody know?28/12 23:40
--- Day changed Wed Dec 29 2010
codoliosully: http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.TypesSummerSchool200729/12 01:34
--- Day changed Thu Dec 30 2010
pigworkerI'm having a peculiar time with coinduction. It looks like the # operator (delay, or thunk) is treated generatively.30/12 02:47
pigworkertry : (P : (Set -> Lazy Set) -> Set1) -> P thunk -> P thunk ; try P p = {!p!}30/12 02:48
pigworkerbut the p won't go, because the two thunks aren't the same30/12 02:49
copumpkinhah, this is awesome: http://snapplr.com/j9m130/12 17:01
Saizancopumpkin: :O where is that from?30/12 17:28
copumpkinan awesome talk30/12 17:28
copumpkinif you're really nice to me, I'll give you a link30/12 17:29
copumpkinokay fine, you can be mean if you insist: http://vimeo.com/1675457430/12 17:29
copumpkinthe audio is oddly out of sync with the video, but I think we'll survive30/12 17:29
Saizanlet's hope30/12 17:30
copumpkinpigworker: who's the guy who showed up in that video at around 35 minute sin?30/12 17:32
Saizan(btw, what is awesome in particular about that screenshot?)30/12 17:32
copumpkinoh, the -------------30/12 17:32
pigworkeris it the "discussant"? edwinb30/12 17:32
copumpkinoh I see!30/12 17:32
copumpkinyeah, he said he wanted to steal your representation30/12 17:33
copumpkinbut that he was worried it wasn't very speedy30/12 17:33
pigworkerit pummels the hell out of implicit syntax30/12 17:34
pigworkerSaizan: how fat I am these days?30/12 17:36
copumpkinpigworker: could you encode families with that representation, using sigma and an equality primitive?30/12 17:37
copumpkinor, what else is missing from the language?30/12 17:37
Saizanpigworker: not much, really :)30/12 17:38
pigworkerI'm trying to remember what I threw in.30/12 17:39
copumpkinpigworker: pi, sigma, nat, zero, one, two30/12 17:39
copumpkinas far as I could see30/12 17:39
pigworkeryeah, dump nat and chuck in indexed W30/12 17:39
pigworkercould add nasty intensional equality fairly easily30/12 17:40
pigworkerwe shouldn't be far off adding indexed induction recursion30/12 17:42
pigworkerI think a Set : Set bootstrap is not far away.30/12 17:42
copumpkinso assuming no Set : Set, what expressive power are you losing that would prevent agda-in-agda?30/12 17:43
djahandarieWhere was this talk given?30/12 17:45
pigworkerdjahandrie: Workshop on Generic Programming, Baltimore, September 201030/12 17:48
djahandarieAh I see. Were there many people there who were familiar with dependent types and Agda?30/12 17:49
pigworkercopumpkin: not sure where it bites, in terms of cranking up a universe hierarchy; it should be possible to build Agda-to-level-n in Agda, without paradox30/12 17:50
copumpkinthat would make sense30/12 17:50
copumpkinmaybe representing (l : Level) -> Set l is where it would break? :P30/12 17:51
pigworkerdjahandrie: The audience was quite mixed in that respect. And it was fairly esoteric stuff. Finding a good level to work at was tricky, but there was good interaction.30/12 17:52
copumpkinpigworker: an unrelated question: do you think there's a relationship between zippers and comonads?30/12 18:03
pigworkeryes30/12 18:03
pigworkerif F is a differentiable functor, then D F * Id is a comonad30/12 18:04
pigworkerthe counit projects out the element in focus; the cojoin shows you all the ways you can refocus30/12 18:05
roconnorcopumpkin: sure but D F * Id isn't a zipper.  A zipper is more like D F * F and even that isn't a zipper.30/12 18:07
pigworkerthe most local layer of a Mu F zipper is a (D F * Id) (Mu F)30/12 18:09
pigworkerthe comonad structure is always going to talk about elements rather than subobjects30/12 18:11
roconnorwhat does "most local layer" mean?  A zipper is either [D F (Mu F)]  or [D F (Mu F)] * (Mu F) depending on your definition of zipper.30/12 18:16
Saizanwith G a = Mu (F a), i've seen D G * Id called the G zipper, and that's a comonad30/12 18:16
roconnorD G?30/12 18:17
Saizanyes30/12 18:17
pigworkerthe latter, and if you're in the cons case (and thus in a position to consider going sideways), the head of the zipper and the term in focus form a (D F * Id) (Mu F)30/12 18:18
pigworkerSaizan: that's a comonad, but it focuses on an a element (anywhere in the tree), not a subtree30/12 18:19
roconnorSaizan: the person who called that a zipper must have been confused.30/12 18:20
pigworkernow, the derivative of a free monad gives a zipper (because you can put an element anywhere you can put a subobject)30/12 18:21
roconnorWhat is the derivative of (s ->)?30/12 18:26
roconnoractually, what is the antiderivative of (s ->)?30/12 18:26
roconnor1/s*((s+1)->) ?30/12 18:27
roconnorah wait nevermind30/12 18:28
pigworkerquotients can make sense of some of those bits and pieces30/12 18:28
pigworkerX^3 is the derivative of a cyclic 4-tuple of X30/12 18:29
roconnorwe need infinite zippers of type Stream (D F (Mu F)) * (Mu F) so that we can always move sideways.30/12 18:32
roconnorgranted these zippers can never be zipped up.30/12 18:33
pigworkerI like the way we're a finite distance from the leaves of an infinite tree. there.30/12 18:33
copumpkinanyone know of anyone who worked on representing substructural typed abstract syntax in agda or a similar language?30/12 19:08
dolioThere was a paper on doing substructural stuff in Twelf not long ago.30/12 19:37
doliohttp://namebinding.wordpress.com/2010/10/14/higher-order-representations-of-substructural-logics/30/12 19:39
pigworkerI've mucked about with linearity.30/12 19:51
pigworkerNow where did I put it?30/12 19:52
copumpkinI was just wondering if there was a nice way to parametrize the representation by which substructural rules you allow, to get the various flavors for free30/12 19:53
copumpkinbut I'd be interested in seeing what you have30/12 19:53
copumpkindolio: thanks, that looks interesting30/12 19:53
pigworkermy trick was to index variable lookup by before-and-after contexts, then thread that through terms30/12 19:54
dolioWell, you couldn't parameterize that technique by what you'd think of as the substructural rules, at least.30/12 19:54
dolioBecause that technique, by necessity, just throws out the idea of linearity (or whatever you're doing) as rules about context manipulation.30/12 19:55
pigworkerone might parametrize by the variable lookup representation (which uses destroy variables, etc) and then check that terms make an acceptable transition (e.g. that they destroy all the variables)30/12 19:57
dolioInstead it defines a 'uses a parameter linearly' predicate on terms.30/12 19:57
pigworkerHere http://personal.cis.strath.ac.uk/~conor/fooling/PCon.agda is a large and grotty example of what I'm talking about.30/12 20:00
dolioManaging the context yourself in some way is the, I guess, obvious solution.30/12 20:04
dolioI was surprised that someone came up with a way to do it in an LF without substructural typing itself.30/12 20:04
copumpkinpigworker: clerical/medical? :O30/12 20:05
pigworkerlame puns: Fr a priest, GP a doctor. Too many crosswords...30/12 20:07
copumpkinoh :)30/12 20:07
* sully needs to take a look at the linear logic in twelf paper and code30/12 20:19
* sully took Constructive Logic from Crary last semester and is TAing CMU's undergrad PL class for him next semester30/12 20:21
* djahandarie hasn't taken his undergrad PL class yet :(30/12 20:36
copumpkinmine wasn't very inspiring30/12 20:37
copumpkinI didn't get into PL stuff until after I graduated :(30/12 20:37
* Saizan wonders what would mean to add constraint programming to twelf30/12 20:58
sullyour PL class is very type theory oriented30/12 20:59
copumpkinsully: ah, I wish I'd had that :)30/12 20:59
sullyand is very much not a "programming language zoo" class, where you go and look at a bunch of real programming languages30/12 21:00
sullythis is unfortunate if that is what you wanted30/12 21:00
sullybut great if you buy into the CMU philosophy on programming languages30/12 21:01
copumpkindo you know if that PL class is offered in the qatar campus of CMU?30/12 21:01
copumpkincause I have a friend there30/12 21:01
ccasinthat class is really great - it made me a PL convert30/12 21:01
copumpkinand really want to get him into this stuff :P30/12 21:01
sullywhich is that type theory is the primary tool that should be used in the study and design of programming languages30/12 21:01
sullywhich I more or less do, so I really liked it30/12 21:01
sullycopumpkin: I'm not sure; I would guess no, but I really have no actual idea30/12 21:02
copumpkinah okay30/12 21:02
copumpkinI don't really know how connected the two are30/12 21:02
ccasinI think they probably have it30/12 21:03
ccasinI bet Iliano teaches it30/12 21:03
sullyhm, I can check.30/12 21:03
sullyyup, they do30/12 21:03
sullytaught by Cervesato30/12 21:03
copumpkinoh nice30/12 21:03
sullyoh, yeah Iliano Cervesato30/12 21:04
* edwinb feels his ears burning30/12 23:40
edwinbAha, the videos...30/12 23:41
edwinbI found the video of my ICFP talk, watched 5 seconds and decided never to look at it again30/12 23:41
pigworkercan't bear to look at mine either30/12 23:46
pigworkerthe best thing about being me at one of my gigs is not having to be in the audience30/12 23:46
edwinbit would probably make me do better talks if I did look. However.30/12 23:47
pigworkertorture...30/12 23:48
edwinbthe odd thing is that the audience were laughing right at the start, but whatever it was I said has been chopped out...30/12 23:48
edwinbor maybe, what the session chair said...30/12 23:48
pigworkerit's like live albums - they always applaud you for putting them on30/12 23:49
edwinbpeople clap when they recognise the song...30/12 23:50
pigworkeran excellent piece of conditioning30/12 23:51
edwinbI don't suppose we can get the audience to clap when we start to talk about Vectors30/12 23:52
edwinb"Oooh! The hit! I know this one!"30/12 23:52

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