# January.log

vixey vixey vixey --- 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 secs 01/01 00:10 -!- You're now known as Laney 01/01 18:32 --- Day changed Fri Jan 02 2009 -!- vixey_ is now known as vixey 02/01 20:59 --- Day changed Sat Jan 03 2009 --- Day changed Sun Jan 04 2009 so what's everything writing in Agda 04/01 20:20 ? 04/01 20:20 everyone* 04/01 20:20 I'm mainly using it to prototype ideas for datatype-generic programming. 04/01 21:09 cool! 04/01 21:09 I just saw in some agda notes the generic fold 04/01 21:09 you mean in Ulf's summer school tutorial? 04/01 21:13 yes 04/01 21:13 yes, that's related 04/01 21:14 I'm working on the multirec library for Haskell (on Hackage) 04/01 21:14 oh I hadn't heard of it 04/01 21:14 I'll look it up 04/01 21:15 I'm thinking about various extensions for it 04/01 21:15 and sometimes (often, actually) it's easier to first code it up in Agda 04/01 21:15 and the worry about how to get everything back into Haskell 04/01 21:15 s/the/then/ 04/01 21:16 hehe 04/01 21:19 after learning a bit about dependent types.. I found some GADT trick in haskell 04/01 21:19 yes, there are various techniques for coding up dependent types 04/01 21:20 involving GADTs and type families (or functional dependencies) 04/01 21:20 but it's all a bit at the border of what ghc can do 04/01 21:20 I've run into more than one limitation or bug doing these things 04/01 21:21 that's why I find Agda easier for prototyping 04/01 21:21 there I can test if the ideas work at all, without worrying about the limitations of the current type system 04/01 21:21 I like Agda but....... I use the emacs mode and it becomes so slow after a couple of times 04/01 21:21 yes, it's still slow 04/01 21:21 there's been a patch recently that improved things a bit 04/01 21:22 but still ... 04/01 21:22 I was reading about the NbE technique 04/01 21:29 apparently it was in some old version like agda light or something ? and it didn't survive 04/01 21:30 but I thought that would be faster 04/01 21:30 it would be interesting to have a quote primitive 04/01 21:34 something that turns a type into it's syntax -- and then you can write a function on that syntax 04/01 21:34 I wonder if it's possible to write a proper tactic prover with it 04/01 21:35 hey this is strange 04/01 21:39 ex'' : (A : Set) -> (P : (A -> A) -> Set) -> (a : A -> A) -> P a -> P ($$x : A) -> (a x)) 04/01 21:40 ex'' A P a Pa = Pa 04/01 21:40 that typecheckes 04/01 21:40 ex''' : (A : Set) -> (P : ((A -> A) -> A -> A) -> Set) -> P (\f -> f) -> P (\f x -> f x) 04/01 21:40 ex''' A prf = prf 04/01 21:40 but this one doesn't 04/01 21:40 it's like it almost does eta conversion .. but not seriously 04/01 21:40 did you see Idris btw? 04/01 21:45 the C FFI is very neat.. 04/01 21:45 very interesting multirec stuff 04/01 21:55 kosmikus, 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 is anyone here? 05/01 02:07 helo? 05/01 02:08 --- Day changed Tue Jan 06 2009 hi. "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 stevan: I haven't actually tried it yet, but I have seen patches in Agda corresponding to this. 06/01 13:59 for instance, two patches by NAD on Dec 17 06/01 14:00 hmm, 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 I wouldn't think so 06/01 14:07 I just checked and it seems I can run "agda Everything.agda" with an up-to-date agda binary 06/01 14:09 thanks 06/01 14:09 hmm, 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 stevan: again, I haven't tried it yet. but maybe you're somehow using an older version of the emacs mode? 06/01 15:09 does it know where to find the std library ? 06/01 15:15 nope, it's the most recent emacs mode. and yes it does find the std lib. :-/ 06/01 15:19 what error do you get? 06/01 15:20 /chalmers/users/stevan/tmp/lib2/Data/Nat.agda:22,18: Parse error # # {-# BUILTIN NATURAL # #... 06/01 15:20 ops, there should be a \-> right before "" 06/01 15:21 the file im trying to load is just "module Test where \n open import Data.Nat" 06/01 15:24 stevan: can you verify in the ghci buffer that it's really the correct Agda version that's being used? 06/01 15:30 otherwise, I'm out of ideas 06/01 15:30 found 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 hi 09/01 08:03 how do you tell agda where to look for libraries? 09/01 09:30 oh.. 09/01 09:32 in the emacs mode it's a variable you can set 09/01 09:32 wonderful......... 09/01 09:33 suc  : (n : ℕ) → ℕ 09/01 09:33 gives: Parse error → ℕ {-# BUILTIN NATURAL ℕ #... 09/01 09:33 hi 09/01 09:33 hey 09/01 09:33 did you recently pull the std lib? 09/01 09:34 yes 09/01 09:34 just this moment 09/01 09:34 did you update agda too? 09/01 09:34 I thought I could save myself the trouble of writing data N : Set where Z : N ; S : N -> N  :D 09/01 09:34 no, should have thought to try that though. thanks 09/01 09:34 i 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 that's pretty strange, I thought a lot of people would be using  \->  in data types 09/01 09:39 of their own definition, I mean.. not instead of the usual -> 09/01 09:39 the old syntax still works, perhaps one can hide the new somehow. 09/01 09:45 --- Day changed Sat Jan 10 2009 how do you turn off the positivity check? 10/01 14:48 wonderful 10/01 15:55 Agda update breaks this code: http://www.cs.nott.ac.uk/~jmc/BSN.html 10/01 15:55 data Ty : Set where 10/01 15:56 N   : Ty 10/01 15:56 _→_ : Ty -> Ty -> Ty 10/01 15:56 that's crazy, Agda is getting as bad as Haskell in terms of back compatability 10/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 secs 11/01 18:19 --- Day changed Mon Jan 12 2009 -!- vixey is now known as vixey 12/01 19:52 --- Day changed Tue Jan 13 2009 --- Day changed Wed Jan 14 2009 -!- eelco__ is now known as eelco 14/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 Beatles 19/01 03:02 -!- _dolio is now known as dolio 19/01 17:56 --- Day changed Tue Jan 20 2009 -!- _dolio is now known as dolio 20/01 07:22 --- Day changed Wed Jan 21 2009 g'day 21/01 11:12 hi 21/01 11:12 i'm having some problems using the latest stdlib, anybody else experienced that? 21/01 11:13 uh.. Just about everyone :p 21/01 11:13 hehe, well, i get parse errors when using it from the command-line, but in interactive mode it works 21/01 11:14 i suspect is has to do with the utf-8 characters 21/01 11:15 recently in the stdlib it changed from -> to the actual arrow symbol 21/01 11:16 (how anybody thought that was a good idea.. I have no clue) 21/01 11:16 but when I got the newer agda it works ok..... 21/01 11:17 maybe you have to update agda 21/01 11:17 no, i just did, interactive mode works, but on the commandline in does stuff like 21/01 11:17 § agda -i ../agda-lib/ problem.agda                                       1 21/01 11:18 Checking Data.Vec ( /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda ) 21/01 11:18 /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18-18 21/01 11:18 /Users/eelco/Archive/Studie/Afstuderen/agda-lib/Data/Vec.agda:20,18: 21/01 11:18 Parse error : a) (xs : Vec a n) → Vec a (su... 21/01 11:18 and yes, i also upgraded the agda executable 21/01 11:18 eelco: 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 recompilation 21/01 14:18 might have been part of the problem, but my install was (somehow) broken anyway, i fixed it by reinstalling from scratch 21/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 secs 23/01 04:31 -!- You're now known as Laney 23/01 11:39 -!- vixey is now known as vixey 23/01 12:06 --- Day changed Sat Jan 24 2009 --- Day changed Sun Jan 25 2009 --- Day changed Mon Jan 26 2009 hello, where can i find refl in the std lib? looking at Data.Bool, for example, import Relation.Binary.PropositionalEquality as PropEq 26/01 10:32 open PropEq using (_#_; refl) 26/01 10:32 it 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 loading Data.Bool.agda works fine tho, how can that be? 26/01 10:35 stevan: Relation.Binary I think 26/01 10:40 import Relation.Binary as Bin    open Bin using (refl)    The module Bin doesn't export the following: refl 26/01 10:42 stevan: mea culpa. Relation.Binary.Core 26/01 10:45 nope :-/ 26/01 10:46 same error 26/01 10:46 actually, PropositionalEquality works for me 26/01 10:46 you probably need to update 26/01 10:46 weird. 26/01 10:47 ok, i ll try to update 26/01 10:47 thanks 26/01 10:47 np 26/01 10:48 hi kosmikus 26/01 16:29 hi vixey 26/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 secs 27/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 hello, can someone explain this to me? http://pastie.org/376070 31/01 17:12 _&_ : Set -> Set -> Set 31/01 17:16 ⊤ & y = y 31/01 17:16 ⊥ & _ = ⊥ 31/01 17:16 is equivalent to 31/01 17:16 _&_ : Set -> Set -> Set 31/01 17:16 x & y = y 31/01 17:16 It's because you can't pattern match on types 31/01 17:16 ah 31/01 17:17 (if you could case dispatch on types, then they could not be erased for runtime) 31/01 17:17 stevan, confused the hell out of me for a few mins though :p 31/01 17:17 but if you try e.g. 31/01 17:17 data Bool : Set where 31/01 17:17 T : Bool 31/01 17:18 F : Bool 31/01 17:18 and rewrite the definition with T/F/Bool instead of ⊤/⊥/Set, you'll see the difference 31/01 17:18 and then a function, 31/01 17:18 decode T = ⊤ 31/01 17:18 decode F = ⊥ 31/01 17:18 decode is the sort of thing you might have 31/01 17:19 so in order to define a _&_ for \top and \bot one has to go thru Bools? 31/01 17:25 no 31/01 17:25 It's just impossible to case dispatch based on _types_ 31/01 17:25 i'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 I don't know what you mean 31/01 17:29 you know my  decode  function 31/01 17:30 it's absolutely impossible to write a  code  function, which is the inverse 31/01 17:30 ok, i think i get it now. :-) 31/01 18:09 thanks 31/01 18:09 hmmm 31/01 19:25 this might explain something weird I came across in the past actually 31/01 19:25 no it doesn't :/ 31/01 19:28 data N : Set where O : N ; S : N -> N 31/01 19:29 data Fin : N -> Set where fz : {n : N} -> Fin (S n) ; fs : {n : N} -> Fin n -> Fin (S n) 31/01 19:29 data Eq (A : Set) : A -> A -> Set where refl : {a : A} -> Eq A a a 31/01 19:29 data Eq1 (A : Set1) : A -> A -> Set1 where refl1 : {a : A} -> Eq1 A a a 31/01 19:29 weird : {n m : N} -> Eq1 Set (Fin n) (Fin m) -> Eq N n m 31/01 19:29 weird refl1 = refl 31/01 19:29 is the weird thing, incase anyone cares 31/01 19:29 you don't get type constructor injectivity in Coq or similar 31/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!