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