February.log

--- Log opened Sun Feb 01 00:00:53 2009
--- Day changed Mon Feb 02 2009
-!- _nano is now known as faXx02/02 19:42
--- Day changed Tue Feb 03 2009
--- Day changed Wed Feb 04 2009
--- Day changed Thu Feb 05 2009
--- Day changed Fri Feb 06 2009
--- Day changed Sat Feb 07 2009
-!- jfredett_ is now known as jfredett07/02 08:37
Cheshirehi07/02 15:43
CheshireThere are a lot of single constructor data types which are interesting like  Eq, Exists, W, Acc, .. what others have I not listed?07/02 15:44
Cheshiredata W (S : Set)(T : S → Set) : Set where07/02 16:08
Cheshire_▹_ : (x : S) → (T x → W S T ) → W S T07/02 16:08
stevando you mean these perhaps? http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.RulesForTheStandardSetFormers07/02 16:12
Cheshirethat is pretty cool07/02 16:13
CheshireI suppose the unit type listed there, I hadn't mentioned07/02 16:13
Cheshireso now I have got 5 one constructor types :)07/02 16:14
Cheshirebtw it says "The choice of identifiers follow largely Martin-Löf Bibliopolis" -- is there any way to access this Bibliopolis?07/02 16:14
stevani don't know, but there are two free books om MLTT listed under publications here: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Documentation07/02 16:21
Cheshirefound another one07/02 17:19
Cheshiredata So : Bool -> Set where oh : So true07/02 17:19
Cheshire(from http://www.cs.nott.ac.uk/~txa/oxford04/ )07/02 17:19
Cheshireoh and JMeq!07/02 17:26
Cheshirethat's 7 now :D07/02 17:27
--- Day changed Sun Feb 08 2009
Cheshiredata T : Set where I : T08/02 14:28
Cheshiredata Eq (A : Set)(x : A) : A -> Set where refl : Eq A x x08/02 14:28
Cheshiredata JMEq (A : Set)(x : A) : (B : Set) -> B -> Set where JMrefl : JMEq A x A x08/02 14:28
Cheshiredata So : Bool -> Set where oh : So true08/02 14:28
Cheshiredata Ex (T : Set)(P : T -> Set) : Set where witness : ((t : T) -> P t) -> Ex T P08/02 14:28
Cheshiredata Acc (A : Set)(R : A -> A -> Set) : A -> Set where below : ((y : A) -> R y x -> Acc A R y) -> Acc A R x08/02 14:28
Cheshiredata W (A : Set)(B : A -> Set) : Set where sup : (a : A)(f : B a -> W A B) -> W A B08/02 14:28
Cheshirethat's all the single constructor inductives I know08/02 14:28
Cheshiretruth, equality, JMequality, the microscopic universe, dependent sum(pair), Accessability/Noetherian-induction, W - well founded trees08/02 14:29
CheshireCan you help me find any more?08/02 14:29
Cheshire(All these guys have got interesting theory and structure that the others don't btw)08/02 14:30
Cheshireaw nobody is alive here08/02 18:17
stevani'm, but i don't know any more of them. :-) why are they of interest to you?08/02 18:29
Cheshirewell they have a special elimination rule08/02 18:33
CheshireIf you have a distinction between types and proofs, like Coq has got types in Set and types in Prop, Agda has Prop too but it's only half implemented08/02 18:33
Cheshireanyway, the idea is that you can't eliminate out from a proof to a type, but you can with single constructor proofs08/02 18:34
Cheshire(you can with zero constructor proofs as well)08/02 18:34
Cheshireso I'm interested in them because I want to think about how this special elimination rule works with each of them08/02 18:34
Cheshirefor example given a proof Prf(a = b) I can construct the actual object a = b08/02 18:35
Cheshirebut given a proof Prf(W A B) I can't always reconstruct the object08/02 18:35
Cheshiresimilary with an existence proof  Prf(Ex A P)  I can't get the object 'a' out but I can get an object []a : Prf(A)08/02 18:38
CheshireI think there must be more in use, but I don't know what they are08/02 18:40
--- Day changed Mon Feb 09 2009
Cheshirehi09/02 14:25
stevanhello09/02 14:58
Cheshirehi09/02 20:51
--- Day changed Tue Feb 10 2009
rwbartonI've just downloaded Agda and am playing around with it from the emacs interface.  Does agda have something like ghci where I can enter and reduce terms and such?10/02 04:41
rwbartonAh, I found it.10/02 05:02
rwbartonAlso, am I a bad person if I want to give all my constructors capitalized names and all my variables lowercase names? :)10/02 05:02
--- Day changed Wed Feb 11 2009
--- Day changed Thu Feb 12 2009
rwbartonwhat does it mean when parts of my program get a yellow background?12/02 07:47
rwbartonThis only happens in my program with --proof-irrelevance; why might that be?12/02 07:47
stevanrwbarton: the yellow part means that the termination-checker isn't happy.12/02 10:42
stevanproofs have to terminate. there is a section in DTs at work describing how the termination checker works. http://www.cs.chalmers.se/~bove/Papers/dep_types.pdf12/02 10:46
swiertstevan: No - yellow means it cannot fill in implicit arguments.12/02 10:46
swiertBrownish-red means it fails the termination check.12/02 10:46
stevanoh12/02 10:47
Cheshirehey swiert12/02 10:48
swierthi Cheshire.12/02 10:49
CheshireI'm just wondering , do you know what's happening with Epigram 2 and OTT?12/02 10:49
swiertNot exactly, no.12/02 10:49
Cheshireit seems that nobody works on Epigram 2 anymore12/02 10:49
swiertEpigram development has slowed down quite a bit.12/02 10:50
swiertConor's moved to Glasgow and has quite a lot of teaching/other responsibilities.12/02 10:50
swiertAnd he hasn't assembled an army of PhD students to work on Epigram 2 just yet.12/02 10:50
Cheshirehehe12/02 10:50
swiertI imagine it may take a while for it to start moving again.12/02 10:51
swiertIn the meantime, I've heard rumours that mattam has plans to implement OTT in Coq...12/02 10:51
Cheshireoo12/02 10:51
CheshireI saw Conors prototype12/02 10:51
swiertYeah - I think people are getting a better understanding of both the theory and implementation of OTT.12/02 10:53
swiertI know there's been a journal version of the original OTT paper in preparation for a while now.12/02 10:54
CheshireI reread the paper and it makes a bit more sense to me.. I think I had to see a color version or something :p12/02 10:54
swiertAnd Conor's prototype seems to suggest that it wouldn't be too hard to implement in the core of a proof assistant that you build from scratch.12/02 10:54
swiertThe idea is actually very simple.12/02 10:55
swiertBut the paper does obscure, I have to admit.12/02 10:55
swiert*obscure this12/02 10:55
-!- jfredett is now known as jF_r_E_d_e_T_t12/02 21:12
-!- jF_r_E_d_e_T_t is now known as jfredett12/02 21:12
CheshireWill Agda change from readline to editline?12/02 23:00
Cheshireactually wait a sec this is a GHC problem12/02 23:00
Cheshirehow do you download  darcs get --partial http://code.haskell.org/Agda12/02 23:04
Cheshirewithout it getting stuck12/02 23:04
Cheshireoh seems the new one uses haskeline12/02 23:14
kosmikusCheshire: yes, it does12/02 23:20
kosmikusCheshire: have you managed to download it?12/02 23:20
CheshireI think I give up trying to compile agda today12/02 23:20
Cheshireyes I got the download but happy is screwed up or something12/02 23:21
kosmikushmm12/02 23:21
kosmikusis it?12/02 23:21
kosmikuswhat version of happy do you have?12/02 23:21
Cheshiretrying to compile happy source with runhaskell gave some undefined reference and trying to install with cabal claims to work but cabal configure in agda repo says I don't have happy12/02 23:22
Laneyjust try "cabal install"12/02 23:22
Cheshire1.18.2 apparently12/02 23:22
Laneymaybe cabal update first12/02 23:22
Cheshirethat says cabal: happy version >=1.15 && <2 is required but it could not be found. as well12/02 23:23
kosmikusyes. I usually do "cabal install" in the Agda dir and it just works for me12/02 23:23
Cheshireyou lot have more luck than me :p12/02 23:23
kosmikushmm, 1.18.2 is newer than what I have, though12/02 23:23
kosmikusI have 1.17 still12/02 23:23
kosmikusso maybe there's something about 1.18.2 that causes problems, but that's pure speculation12/02 23:23
* Laney too12/02 23:23
kosmikussince happy is a cabal package, I'm surprised that "cabal install" doesn't just install it if it thinks it's not there12/02 23:25
Cheshireyes it's weird12/02 23:26
kosmikuslet's see, I'm upgrading happy now12/02 23:26
CheshireI'll try te build happy from source code instead of cabal12/02 23:27
kosmikuswhat happens if you say "cabal install happy" ?12/02 23:27
Cheshireit gives a lot of warnings about incomplete pattern matches and stuff but it claims to have installed happy12/02 23:28
kosmikusok, and typing "cabal install" in the Agda darcs directory claims to not have happy?12/02 23:28
Cheshireyes exactly12/02 23:28
kosmikusI really mean "cabal install", not "cabal configure" ...12/02 23:29
Cheshireit is a complete lie...12/02 23:29
Cheshireboth cabal install and cabal configure say I don't have happy12/02 23:29
kosmikuswhich OS?12/02 23:29
Cheshiremac os12/02 23:29
kosmikusdo you have $HOME/.cabal/bin in your $PATH?12/02 23:30
Cheshireno :D12/02 23:30
kosmikusok12/02 23:31
Cheshirethank you so much kosmikus, that allows it to build12/02 23:31
kosmikuscool12/02 23:31
kosmikusyes, it's one of the common pitfalls of cabal install12/02 23:31
kosmikusit should more prominently tell you to put that dir in your search path12/02 23:31
kosmikusso, the build succeeded also with happy-1.18.2 here, so you should be fine ...12/02 23:33
Cheshireyay it works12/02 23:46
Cheshirehad to change some emacs font thing too which sucked12/02 23:46
--- Day changed Fri Feb 13 2009
rwbartonIf I have data _≡_ {a : Set} (x : a) : a -> Prop where refl : x ≡ x, can I write ≡-ext : {a c : Set} {x y : c -> a} -> ((u : c) -> x u ≡ y u) -> _≡_ {c -> a} (\u -> x u) (\u -> y u) ?  (equality of functions is extensional)13/02 06:38
rwbartonin fact, just rewrite that last type as x ≡ y13/02 06:39
CheshireI wish there were one channel for all dependent types :?13/02 18:25
Cheshirewell afaik there is 2 channels13/02 18:26
Cheshiresince nobody in Coq talks ..  does anyone here know some ways to write dependent generic programs?13/02 19:38
Cheshireit's pretty straightforward to write generic functions like T : Φ -> Set, but what about stuff like F : (o : Φ) -> T o  ?13/02 19:39
CheshireΦ being a type from some fixed universe13/02 19:40
CheshireHere is a good paper about it btw13/02 22:14
Cheshirehttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.914413/02 22:14
--- Day changed Sat Feb 14 2009
Cheshirehttp://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=18714/02 22:22
Cheshiredoes14/02 22:22
CheshireAgda’s termination checker isn’t so good at spotting that this is what’s going on, but before we had Agda’s bag on the side, there was a language called Epigram which resorted to Type Theory as its language for explaining termination. Gasp!14/02 22:22
Cheshiremean that they are not making Epigram?14/02 22:22
--- Day changed Sun Feb 15 2009
Cheshirehey15/02 15:13
Cheshiregreat news, Agda has got the eta rule!15/02 15:13
CheshireI was just looking at the source code yesterday... turns out they have type directed conversion checking15/02 15:13
Cheshireso now you can write:15/02 15:14
Cheshirecont-left-identity : forall {a b r} -> (o : a) -> (f : a -> cont b r) -> (return o >>= f) == f o15/02 15:14
Cheshirecont-left-identity o f = refl (f o)15/02 15:14
Cheshirecont-right-identity : forall {a r} -> (n : cont a r) -> (n >>= return) == n15/02 15:14
Cheshirecont-right-identity n = refl n15/02 15:14
Cheshirecont-associativity : forall {a b c r} -> (n : cont a r) -> (f : a -> cont b r) -> (g : b -> cont c r) -> ((n >>= f) >>= g) == (n >>= (\x -> (f x) >>= g))15/02 15:14
Cheshirecont-associativity n f g = refl ((n >>= f) >>= g)15/02 15:14
Cheshireall the Cont monad proofs are trivial :15/02 15:14
Cheshirewhereas in Coq you have to accept an eta axiom.. and basically implement type directed eta conv. as a tactic15/02 15:14
ski__that's nice15/02 15:44
* ski__ was trying to fathom `forall a b. (\(f a) -> a) = (\(f b) -> b)', recently15/02 15:45
Cheshirewhat can this mean?  \(f a) -> ...15/02 15:46
Cheshireyou are taking the inverse of f?15/02 15:47
ski__in some sense, yes15/02 15:49
ski__i'm trying to follow a notion/principle through any craziness it might lead me into15/02 15:50
Cheshireone of the examples for pattern matching on inductive families was a inverse-witness sort of type -- matching on it would give you proof of inverse15/02 15:50
ski__however, i can't say i really understand where this is taking me, atm15/02 15:50
Cheshirein i.e. eliminating dependent pattern matching15/02 15:50
Cheshire but you have to construct the inverse to get an object of that type15/02 15:50
ski__(if you wonder, the above proposition is meant to claim that `f' is injective)15/02 15:51
ski__(it's just an example of what i'm trying to think about)15/02 15:51
Cheshireis there any relational (as opposed to functional) analogue of lambda calculus?15/02 15:52
ski__  data ImageElem {A B : Set} (f : A -> B) : B -> Set15/02 15:53
ski__    where15/02 15:53
ski__    IE : (a : A) -> ImageElem f (f a)15/02 15:53
ski__was it something like that ?15/02 15:53
Cheshireyes exactly15/02 15:53
ski__i suppose it depends on what you mean by "analogue of lambda calculus"15/02 15:54
ski__i don't know of any nice primitives that are per se computable15/02 15:54
ski__but i think "The Algebra of Programming" by Bird and Meertens (iirc) mentions reasoning in an allegory to derive algorithms from specifications, for relations15/02 15:55
ski__(function : category :: relation :: allegory)15/02 15:55
Cheshirereals : functions :: complex numbers : relations15/02 15:56
Cheshire:)15/02 15:56
ski__(um, replace the latter `::' by `:' .. it was meant as a double proportion)15/02 15:57
ski__Cheshire : really ?15/02 15:57
Cheshirewe can't construct e.g. solutions to cubics without going via complex numbers15/02 15:57
Cheshireand some proofs, or derivations they use relations in a similar way -- even though the end result is a function15/02 15:58
ski__(an allegory is basically a category having a few more operations and satisfying some more laws, that make the "morphisms" behave a lot like binary relations)15/02 15:58
ski__ah, ok15/02 15:58
Cheshireand complex/imaginary numbers not being something you can measure is why people use want real eigenvalues etc.. so the analogue there would be with functions being computable (useful) and relations not being.. I suppose15/02 15:59
ski__i think one could possibly make computable relations .. think something like pure Prolog, but an abstract theory behind that15/02 16:00
ski__computable might mean that for each input, we can enumerate the outputs15/02 16:01
ski__or it might mean that we can cut away larger and larger parts of the output solution space, thereby removing points which can't be outputs15/02 16:01
ski__probably one should also consider "running a relation backwards" in such a theory15/02 16:02
* ski__ though has no idea how to make such a theory :/15/02 16:02
CheshireI think you really need to support all 4 modes for every binary relation15/02 16:02
Cheshire++ +- -+ --15/02 16:02
ski__i'm not sure of that .. as long as you keep track of which modes are admitted for which relations15/02 16:03
Cheshirehm15/02 16:03
Cheshireif you compose some relations like  xRR'R''y15/02 16:03
ski__then one needs to check which modes are still possible here, yes15/02 16:03
CheshireR' doesn't necessarily run in -- mode, since you could feed values into via solutions from R and/or R''15/02 16:03
* ski__ thinks a type-system that requires `e' in the application `e e0' to be of form `\p0 -> e1' to be weird ..15/02 16:16
Cheshirebbl15/02 16:17
--- Log closed Sun Feb 15 17:50:50 2009
--- Log opened Sun Feb 15 17:58:44 2009
-!- Irssi: #agda: Total of 12 nicks [0 ops, 0 halfops, 0 voices, 12 normal]15/02 17:58
-!- Irssi: Join to #agda was synced in 107 secs15/02 18:00
stevanhmm, lhs2tex doesn't seem to like my utf8 comments. is there a simple way around this?15/02 20:51
swiertstevan: which lhs2TeX version are you using?15/02 20:53
stevan1.1415/02 20:55
stevanperhaps i should try the svn version?15/02 20:55
swiertstevan: hmm. I'm not sure that would make a difference.15/02 20:56
swiertutf8 support was only added fairly recently.15/02 20:56
swiertI think I've run into something similar.15/02 20:56
swiertIIRC, formatting directives do not affect comments.15/02 20:57
stevanok15/02 20:59
swiertI think comments may need to be plain ascii, but I'm not entirely sure.15/02 20:59
--- Day changed Mon Feb 16 2009
--- Day changed Tue Feb 17 2009
Cheshirehi17/02 18:30
Cheshirewhat does everyone use induction-recursion for ?17/02 18:30
Cheshirewhere you go17/02 18:30
Cheshiremutual17/02 18:30
Cheshire data ...17/02 18:30
Cheshire f : ...17/02 18:30
Cheshireetc17/02 18:30
Cheshire?17/02 18:30
CheshireI think I saw two times people have used it to formalize a dependently typed language17/02 18:31
Cheshiredoes anyone have more examples?17/02 18:31
Cheshirethere is also some examples around like fresh lists and universes17/02 18:31
Cheshireoh another one is computability predicates17/02 21:51
Cheshirebut that can't be all (?)17/02 21:51
--- Day changed Wed Feb 18 2009
Cheshireoh maybe Agda people could have thought about this too ..?18/02 16:36
Cheshire(is there any typed notion of structurally smaller term?)18/02 16:36
Cheshirejjustout of curiousity18/02 19:21
CheshireX !=< _918/02 19:21
Cheshirewhen checking that the expression A has type _918/02 19:21
Cheshireis that supposed to mean something?18/02 19:21
Cheshireit woul make sense to say e.g.  X is not a set18/02 19:22
--- Day changed Thu Feb 19 2009
sema4rhi. i'm using the debian packages agda and agda-stdlib, pointed to in the wiki. i couldn't get agda-mode installed because of unresolved dependencies from libghc6-agda-dev, so i'm using agda-mode from source.19/02 15:46
sema4reverything seems to work fine except for syntax highlighting in emacs despite font-lock activated.19/02 15:47
sema4rany ideas why that is ?19/02 15:47
sema4roh, i'm using emacs 23 from cvs ...19/02 15:48
rwbartonSyntax highlighting doesn't happen until you load a file into agda, is that it?19/02 16:42
sema4rrwbarton: when i open an agda-file in emacs, the agda2-mode is loaded (if it isn't already) but no syntax highlighting.19/02 16:47
Laneysema4r: You need to load the file (c-c c-l)19/02 16:48
rwbartonI have some emacs mode issues of my own :)19/02 16:51
rwbartonThe agda2-give command (C-c C-SPC) doesn't work properly for me, it typechecks the expression I give it but when that succeeds it doesn't put it into the goal I was in.19/02 16:52
rwbartonIt typically just inserts a space, or some parentheses and spaces.19/02 16:52
rwbartonIs that a known issue?19/02 16:52
sema4rLaney: did that. no difference.19/02 16:59
rwbartonsema4r: When you load the file, does a second window with the *All Goals* buffer appear at the bottom?19/02 17:07
sema4r no. there is something written to a file in /tmp, which is erased immediately afterward. there is some output from the ghci, complaining about unknown package agda too.19/02 17:14
rwbartonAh19/02 17:15
rwbartonSo you don't have agda installed properly19/02 17:15
sema4ri installed agda from the debian repo, advertised on the agda wiki page.19/02 17:17
rwbartonYou need the libghc6-agda-dev package to install correctly19/02 17:19
rwbartonBTW if you have cabal-install installed then it's nearly trivial to build from source19/02 17:19
sema4ri just checked. the libghc6-agda-dev package from that repo has some unresolved dependencies. will wipe the packages of the disk and go via cabal.19/02 17:24
--- Day changed Fri Feb 20 2009
--- Log closed Fri Feb 20 06:30:07 2009
--- Log opened Fri Feb 20 09:58:21 2009
-!- Irssi: #agda: Total of 9 nicks [0 ops, 0 halfops, 0 voices, 9 normal]20/02 09:58
-!- Irssi: Join to #agda was synced in 100 secs20/02 09:59
Cheshirehi20/02 17:58
Cheshiredoes anyone have/know of some formulation liek Acc http://www.cs.nott.ac.uk/~nad/listings/lib/Induction.Nat.html20/02 17:58
Cheshireexcept it works for inductive families (such as Fin and so on)20/02 17:58
--- Day changed Sat Feb 21 2009
-!- eelco_ is now known as eelco21/02 12:18
Cheshireodd21/02 15:56
Cheshiredata le : N -> N -> Prop where21/02 15:56
Cheshire le_O : (x : N) -> le O x21/02 15:56
Cheshire le_S : (x : N) -> (y : N) -> le x y -> le (S x) (S y)21/02 15:56
Cheshiresays,21/02 15:57
CheshireThe type of the constructor does not fit in the sort of the21/02 15:57
Cheshiredatatype, since Set is not less or equal than Prop21/02 15:57
Cheshirewhen checking the constructor le_O in the declaration of le21/02 15:57
Cheshirebut e.g.21/02 15:57
CheshireCoq < Print le.21/02 15:57
CheshireInductive le (n : nat) : nat -> Prop :=21/02 15:57
Cheshire    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m21/02 15:57
Cheshirealso now I realize my definition is wrong but that's really important21/02 15:57
Cheshire(not that I can think of any non-structurally recursive programs thaht would be written over inductive familiess.. does anyone know of some?)21/02 20:58
--- Day changed Sun Feb 22 2009
--- Day changed Mon Feb 23 2009
maltemIn http://www.cs.nott.ac.uk/~nad/listings/lib/Algebra.html some algebraic structures are defined as records. But there are also some record values, e. g. semigroup = record { ... }. What do those mean?23/02 10:11
maltemAh, I realize now they state things like "Every group is a semigroup"23/02 10:23
maltemOn another note, is the stdlib repo broken?23/02 10:28
* Cheshire thinks about renaming Set to Small and Set1 to Big ..23/02 22:09
--- Day changed Tue Feb 24 2009
--- Day changed Wed Feb 25 2009
Tobsan:o25/02 00:42
Cheshirehi25/02 15:00
Cheshireis there any new papers or programs in/about agda or something ?25/02 15:01
--- Day changed Thu Feb 26 2009
-!- jfredett_ is now known as jfredett26/02 01:43
--- Day changed Fri Feb 27 2009
Cheshiredid anyone implement a tactic system inside agda?27/02 17:09
--- Day changed Sat Feb 28 2009
--- Log closed Sun Mar 01 00:00:24 2009

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