January.log

--- Log opened Thu Jan 01 00:09:20 2009
-!- Irssi: #agda: Total of 11 nicks [0 ops, 0 halfops, 0 voices, 11 normal]01/01 00:09
-!- Irssi: Join to #agda was synced in 99 secs01/01 00:10
-!- You're now known as Laney01/01 18:32
--- Day changed Fri Jan 02 2009
-!- vixey_ is now known as vixey02/01 20:59
--- Day changed Sat Jan 03 2009
--- Day changed Sun Jan 04 2009
vixeyso what's everything writing in Agda04/01 20:20
vixey?04/01 20:20
vixeyeveryone*04/01 20:20
kosmikusI'm mainly using it to prototype ideas for datatype-generic programming.04/01 21:09
vixeycool!04/01 21:09
vixeyI just saw in some agda notes the generic fold04/01 21:09
kosmikusyou mean in Ulf's summer school tutorial?04/01 21:13
vixeyyes04/01 21:13
kosmikusyes, that's related04/01 21:14
kosmikusI'm working on the multirec library for Haskell (on Hackage)04/01 21:14
vixeyoh I hadn't heard of it04/01 21:14
vixeyI'll look it up04/01 21:15
kosmikusI'm thinking about various extensions for it04/01 21:15
kosmikusand sometimes (often, actually) it's easier to first code it up in Agda04/01 21:15
kosmikusand the worry about how to get everything back into Haskell04/01 21:15
kosmikuss/the/then/04/01 21:16
vixeyhehe04/01 21:19
vixeyafter learning a bit about dependent types.. I found some GADT trick in haskell04/01 21:19
kosmikusyes, there are various techniques for coding up dependent types04/01 21:20
kosmikusinvolving GADTs and type families (or functional dependencies)04/01 21:20
kosmikusbut it's all a bit at the border of what ghc can do04/01 21:20
kosmikusI've run into more than one limitation or bug doing these things04/01 21:21
kosmikusthat's why I find Agda easier for prototyping04/01 21:21
kosmikusthere I can test if the ideas work at all, without worrying about the limitations of the current type system04/01 21:21
vixeyI like Agda but....... I use the emacs mode and it becomes so slow after a couple of times04/01 21:21
kosmikusyes, it's still slow04/01 21:21
kosmikusthere's been a patch recently that improved things a bit04/01 21:22
kosmikusbut still ...04/01 21:22
vixeyI was reading about the NbE technique04/01 21:29
vixeyapparently it was in some old version like agda light or something ? and it didn't survive04/01 21:30
vixeybut I thought that would be faster04/01 21:30
vixeyit would be interesting to have a quote primitive04/01 21:34
vixeysomething that turns a type into it's syntax -- and then you can write a function on that syntax04/01 21:34
vixeyI wonder if it's possible to write a proper tactic prover with it04/01 21:35
vixeyhey this is strange04/01 21:39
vixeyex'' : (A : Set) -> (P : (A -> A) -> Set) -> (a : A -> A) -> P a -> P (\(x : A) -> (a x))04/01 21:40
vixeyex'' A P a Pa = Pa04/01 21:40
vixeythat typecheckes04/01 21:40
vixeyex''' : (A : Set) -> (P : ((A -> A) -> A -> A) -> Set) -> P (\f -> f) -> P (\f x -> f x)04/01 21:40
vixeyex''' A prf = prf04/01 21:40
vixeybut this one doesn't04/01 21:40
vixeyit's like it almost does eta conversion .. but not seriously04/01 21:40
vixeydid you see Idris btw?04/01 21:45
vixeythe C FFI is very neat..04/01 21:45
vixeyvery interesting multirec stuff04/01 21:55
vixeykosmikus, do you think there are any features (other than efficiency) which Agda misses out on ?04/01 22:13
--- Day changed Mon Jan 05 2009
Marshall_is anyone here?05/01 02:07
Marshall_helo?05/01 02:08
--- Day changed Tue Jan 06 2009
stevanhi. "Sun Jan  4 21:17:31 CET 2009  Nils Anders Danielsson: * Switched from (forall, ->, \) to (\forall, \->, \lambda)."   has anyone got that working? without it, i can use std libs just fine. with it, i get errors around the \->s. i didn't see any corresponding patch for agda itself. could it be that agda isn't ready for this change yet or i'm doing something wrong perhaps? thanks.06/01 13:56
kosmikusstevan: I haven't actually tried it yet, but I have seen patches in Agda corresponding to this.06/01 13:59
kosmikusfor instance, two patches by NAD on Dec 1706/01 14:00
stevanhmm, forgot about those -- been pulling since. i wonder what i managed to mess up then. i used a more recent haskeline than the one enforced by agdas cabal file... but that shouldn't affect loading of files?06/01 14:06
kosmikusI wouldn't think so06/01 14:07
kosmikusI just checked and it seems I can run "agda Everything.agda" with an up-to-date agda binary06/01 14:09
stevanthanks06/01 14:09
stevanhmm, odd. "agda Everything.agda" works for me too. but i get errors when trying to load a module which uses the std lib from emacs...06/01 14:58
kosmikusstevan: again, I haven't tried it yet. but maybe you're somehow using an older version of the emacs mode?06/01 15:09
vixeydoes it know where to find the std library ?06/01 15:15
stevannope, it's the most recent emacs mode. and yes it does find the std lib. :-/06/01 15:19
kosmikuswhat error do you get?06/01 15:20
stevan/chalmers/users/stevan/tmp/lib2/Data/Nat.agda:22,18: Parse error #<ERROR> # {-# BUILTIN NATURAL # #...06/01 15:20
stevanops, there should be a \-> right before "<ERROR>"06/01 15:21
stevanthe file im trying to load is just "module Test where \n open import Data.Nat"06/01 15:24
kosmikusstevan: can you verify in the ghci buffer that it's really the correct Agda version that's being used?06/01 15:30
kosmikusotherwise, I'm out of ideas06/01 15:30
stevanfound the problem. i had hidden the old package in ghc, apparently that wasn't enough -- after unregistering it, it works. thanks for the help. :-)06/01 15:36
--- Day changed Wed Jan 07 2009
--- Day changed Thu Jan 08 2009
--- Day changed Fri Jan 09 2009
vixeyhi09/01 08:03
vixeyhow do you tell agda where to look for libraries?09/01 09:30
vixeyoh..09/01 09:32
vixeyin the emacs mode it's a variable you can set09/01 09:32
vixeywonderful.........09/01 09:33
vixey  suc  : (n : ℕ) → ℕ09/01 09:33
vixeygives: Parse error →<ERROR> ℕ {-# BUILTIN NATURAL ℕ #...09/01 09:33
stevanhi09/01 09:33
vixeyhey09/01 09:33
stevandid you recently pull the std lib?09/01 09:34
vixeyyes09/01 09:34
vixeyjust this moment09/01 09:34
stevandid you update agda too?09/01 09:34
vixeyI thought I could save myself the trouble of writing data N : Set where Z : N ; S : N -> N  :D09/01 09:34
vixeyno, should have thought to try that though. thanks09/01 09:34
stevani think it's this patch to the std lib causing it: Sun Jan  4 21:17:31 CET 2009  Nils Anders Danielsson: * Switched from (forall, ->, \) to (\forall, \->, \lambda)... agda itself was patched 17th dec to handle this.09/01 09:38
vixeythat's pretty strange, I thought a lot of people would be using  \->  in data types09/01 09:39
vixeyof their own definition, I mean.. not instead of the usual ->09/01 09:39
stevanthe old syntax still works, perhaps one can hide the new somehow.09/01 09:45
--- Day changed Sat Jan 10 2009
vixeyhow do you turn off the positivity check?10/01 14:48
vixeywonderful10/01 15:55
vixeyAgda update breaks this code: http://www.cs.nott.ac.uk/~jmc/BSN.html10/01 15:55
vixeydata Ty : Set where10/01 15:56
vixey  N   : Ty10/01 15:56
vixey  _→_ : Ty -> Ty -> Ty10/01 15:56
vixeythat's crazy, Agda is getting as bad as Haskell in terms of back compatability10/01 15:56
--- Day changed Sun Jan 11 2009
--- Log closed Sun Jan 11 17:35:10 2009
--- Log opened Sun Jan 11 18:19:15 2009
-!- Irssi: #agda: Total of 10 nicks [0 ops, 0 halfops, 0 voices, 10 normal]11/01 18:19
-!- Irssi: Join to #agda was synced in 0 secs11/01 18:19
--- Day changed Mon Jan 12 2009
-!- vixey` is now known as vixey12/01 19:52
--- Day changed Tue Jan 13 2009
--- Day changed Wed Jan 14 2009
-!- eelco__ is now known as eelco14/01 11:18
--- Day changed Thu Jan 15 2009
--- Day changed Fri Jan 16 2009
--- Day changed Sat Jan 17 2009
--- Day changed Sun Jan 18 2009
--- Day changed Mon Jan 19 2009
* kerlo sings "Hello Goodbye" by The Beatles19/01 03:02
-!- _dolio is now known as dolio19/01 17:56
--- Day changed Tue Jan 20 2009
-!- _dolio is now known as dolio20/01 07:22
--- Day changed Wed Jan 21 2009
eelcog'day21/01 11:12
vixeyhi21/01 11:12
eelcoi'm having some problems using the latest stdlib, anybody else experienced that?21/01 11:13
vixeyuh.. Just about everyone :p21/01 11:13
eelcohehe, well, i get parse errors when using it from the command-line, but in interactive mode it works21/01 11:14
eelcoi suspect is has to do with the utf-8 characters21/01 11:15
vixeyrecently in the stdlib it changed from -> to the actual arrow symbol21/01 11:16
vixey(how anybody thought that was a good idea.. I have no clue)21/01 11:16
vixeybut when I got the newer agda it works ok.....21/01 11:17
vixeymaybe you have to update agda21/01 11:17
eelcono, i just did, interactive mode works, but on the commandline in does stuff like21/01 11:17
eelco§ agda -i ../agda-lib/ problem.agda                                       121/01 11:18
eelcoChecking Data.Vec ( /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda )21/01 11:18
eelco/Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18-1821/01 11:18
eelco/Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18:21/01 11:18
eelcoParse error :<ERROR> a) (xs : Vec a n) → Vec a (su...21/01 11:18
eelcoand yes, i also upgraded the agda executable21/01 11:18
kosmikuseelco: are you really sure that you upgraded the executable? just typing cabal install in that directory usually is not enough, you should touch Main.hs before doing that to ensure recompilation21/01 14:18
eelcomight have been part of the problem, but my install was (somehow) broken anyway, i fixed it by reinstalling from scratch21/01 14:28
--- Day changed Thu Jan 22 2009
--- Log closed Fri Jan 23 04:25:39 2009
--- Log opened Fri Jan 23 04:29:53 2009
-!- Irssi: #agda: Total of 7 nicks [0 ops, 0 halfops, 0 voices, 7 normal]23/01 04:29
-!- Irssi: Join to #agda was synced in 94 secs23/01 04:31
-!- You're now known as Laney23/01 11:39
-!- vixey` is now known as vixey23/01 12:06
--- Day changed Sat Jan 24 2009
--- Day changed Sun Jan 25 2009
--- Day changed Mon Jan 26 2009
stevanhello, where can i find refl in the std lib? looking at Data.Bool, for example, import Relation.Binary.PropositionalEquality as PropEq26/01 10:32
stevanopen PropEq using (_#_; refl)26/01 10:32
stevanit seems to be in PropEq, but when i try to do the same thing in my own module i get an error saying refl isn't exported by PropEq...26/01 10:33
stevanloading Data.Bool.agda works fine tho, how can that be?26/01 10:35
Laneystevan: Relation.Binary I think26/01 10:40
stevanimport Relation.Binary as Bin    open Bin using (refl)    The module Bin doesn't export the following: refl26/01 10:42
Laneystevan: mea culpa. Relation.Binary.Core26/01 10:45
stevannope :-/26/01 10:46
stevansame error26/01 10:46
Laneyactually, PropositionalEquality works for me26/01 10:46
Laneyyou probably need to update26/01 10:46
stevanweird.26/01 10:47
stevanok, i ll try to update26/01 10:47
stevanthanks26/01 10:47
Laneynp26/01 10:48
vixeyhi kosmikus26/01 16:29
kosmikushi vixey26/01 16:57
--- Day changed Tue Jan 27 2009
--- Log closed Tue Jan 27 05:27:05 2009
--- Log opened Tue Jan 27 05:41:15 2009
-!- Irssi: #agda: Total of 5 nicks [0 ops, 0 halfops, 0 voices, 5 normal]27/01 05:41
-!- Irssi: Join to #agda was synced in 79 secs27/01 05:42
--- Day changed Wed Jan 28 2009
--- Day changed Thu Jan 29 2009
--- Day changed Fri Jan 30 2009
--- Day changed Sat Jan 31 2009
stevanhello, can someone explain this to me? http://pastie.org/37607031/01 17:12
vixey_&_ : Set -> Set -> Set31/01 17:16
vixey⊤ & y = y31/01 17:16
vixey⊥ & _ = ⊥31/01 17:16
vixeyis equivalent to31/01 17:16
vixey_&_ : Set -> Set -> Set31/01 17:16
vixeyx & y = y31/01 17:16
vixeyIt's because you can't pattern match on types31/01 17:16
stevanah31/01 17:17
vixey(if you could case dispatch on types, then they could not be erased for runtime)31/01 17:17
vixeystevan, confused the hell out of me for a few mins though :p31/01 17:17
vixeybut if you try e.g.31/01 17:17
vixeydata Bool : Set where31/01 17:17
vixey T : Bool31/01 17:18
vixey F : Bool31/01 17:18
vixeyand rewrite the definition with T/F/Bool instead of ⊤/⊥/Set, you'll see the difference31/01 17:18
vixeyand then a function,31/01 17:18
vixeydecode T = ⊤31/01 17:18
vixeydecode F = ⊥31/01 17:18
vixeydecode is the sort of thing you might have31/01 17:19
stevanso in order to define a _&_ for \top and \bot one has to go thru Bools?31/01 17:25
vixeyno31/01 17:25
vixeyIt's just impossible to case dispatch based on _types_31/01 17:25
stevani'm confused, i got two \bot / \top values and i want to do the equivalent of _&_ on those. how would i go about?31/01 17:29
vixeyI don't know what you mean31/01 17:29
vixeyyou know my  decode  function31/01 17:30
vixeyit's absolutely impossible to write a  code  function, which is the inverse31/01 17:30
stevanok, i think i get it now. :-)31/01 18:09
stevanthanks31/01 18:09
vixeyhmmm31/01 19:25
vixeythis might explain something weird I came across in the past actually31/01 19:25
vixeyno it doesn't :/31/01 19:28
vixeydata N : Set where O : N ; S : N -> N31/01 19:29
vixeydata Fin : N -> Set where fz : {n : N} -> Fin (S n) ; fs : {n : N} -> Fin n -> Fin (S n)31/01 19:29
vixeydata Eq (A : Set) : A -> A -> Set where refl : {a : A} -> Eq A a a31/01 19:29
vixeydata Eq1 (A : Set1) : A -> A -> Set1 where refl1 : {a : A} -> Eq1 A a a31/01 19:29
vixeyweird : {n m : N} -> Eq1 Set (Fin n) (Fin m) -> Eq N n m31/01 19:29
vixeyweird refl1 = refl31/01 19:29
vixeyis the weird thing, incase anyone cares31/01 19:29
vixeyyou don't get type constructor injectivity in Coq or similar31/01 19:29
--- Log closed Sun Feb 01 00:00:53 2009

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