/home/laney/.irssi/irclogs/Freenode/#agda.log-20170408

--- Day changed Fri Apr 07 2017
quchenWhy is it so hard to work with addition defined as07/04 09:58
quchen_+_ : ℕ → ℕ → ℕ07/04 09:58
quchenzero   + n = n07/04 09:58
quchensucc n + m = n + succ m07/04 09:58
quchenIs the form of recursion »strange« in a way that makes using it for proofs more difficult?07/04 09:58
quchenI’m having lots of trouble showing that this is equivalent to the usual definition of addition, for example07/04 09:59
adamsequchen: http://lpaste.net/4750809024281182208 the proof of equivalence07/04 10:23
quchenadamse: Hm, thanks for the proof. With this equivalence, the rest of the theorems is quite easy.07/04 12:20
quchenBut still, I’m wondering what makes this definition not the go-to definition for natural number addition. I’ve never seen it used anywhere, in fact.07/04 12:21
gallaisquchen: it's not productive.07/04 12:35
quchengallais: Ah, that’s a topic I haven’t touched yet: productive (co-) recursion, right?07/04 12:35
gallaisit just means that it doesn't spit out constructors as it goes07/04 12:36
quchengallais: Do you have some reference to read more about this?07/04 12:38
quchenI tried searching for it, but found only fairly superficial blog posts07/04 12:38
gallaisI guess this is the appropriate notion of addition to define rev-append (aka the auxiliary function for the accumulator-based rev)07/04 12:39
quchenAh, Norell’s book has a section about this (specific example).07/04 12:40
gallaisHmmm. Not quite. You still have to add a rewrite to quickstart the evaluation07/04 12:41
lpastegallais pasted “RevAppend” at http://lpaste.net/35440307/04 12:41
gallaisquchen: not really. I guess most texts will focus on the coinductive case07/04 12:45
gallaisalthough you may be able to find some things if you look for "tail call optimisation" and "haskell": in a lot of situations, it's actually preferable to *not* have tail calls in haskell because productivity & lazyness work well together07/04 12:46
quchenAlong the lines of tail recursion modulo cons?07/04 12:47
gallaise.g. `zip [0] (map f longlist)` will return immediately for a productive `map` and take a long time if `map` is implemented using an accumulator because you'll have to go through the *whole* process of mapping before getting the head of the resulting list07/04 12:47
mietekUNIX pipes07/04 12:48
quchenI’m (very) familiar with Haskell; but it doesn’t have the issues with termination that Agda has, so we never really have to think about it explicitly apart from performance reasons07/04 12:49
quchenIn Agda, the scenario is a bit different: performance is secondary to correctness07/04 12:49
mietekHaskell conflates laziness and corecursion07/04 12:49
mietekthis makes things more confusing than they need be07/04 12:49
quchenI don’t even know how to fomulare Haskell’s [1..] in Agda, although it’s apparently possible07/04 12:49
quchenVia identifying it as a productively corecursive function07/04 12:50
quchenI don’t even know what corecursion is, exactly. »Like an unfold« is as far as I’ve come so far.07/04 12:50
mietekperhaps this pseudocode will help: https://gist.github.com/mietek/068092bae201e42e65ff51791bbd8a3607/04 12:53
mietekI define an ordinary List datatype, and two ways to fold it, one less general, and one more general07/04 12:54
mietekthen, I define a Stream codatatype, and two ways to unfold it, using copattern notation07/04 12:54
mietek_×_ is product, _+_ is sum07/04 12:55
mietekit’s written in this fashion to reveal the duality07/04 12:55
mietek_,_ is the product constructor, case is the sum eliminator07/04 12:56
mieteka datatype is defined by the methods with which we can construct it, cons and nil07/04 12:56
mieteka codatatype is defined by the methods with which we can eliminate it, hd and tl07/04 12:57
mietekStream promises that there will always be a head to observe07/04 12:57
mietekso, if we want to unfold a Stream, we have to provide a result for this observation07/04 12:57
mieteksimilarly with tail; this motivates the copattern notation07/04 12:57
mieteknow, as far as I understand, you can work with codata perfectly well without laziness; however, Haskell’s laziness means that all(?) data is actually codata07/04 13:02
mietek(at least, by default)07/04 13:02
mietekhow to formulate [1..] using an explicit unfold:07/04 13:03
mietekunfoldr :: (b -> Maybe (a, b)) -> b -> [a]07/04 13:03
mietektake 10 (unfoldr (\n -> Just (n+1, n+1)) 0)07/04 13:04
mietekwe start with a seed of 007/04 13:05
mietekit becomes our state07/04 13:05
mietekat every step of the corecursion, we have access to the current state07/04 13:05
mietekat every step, we increment the number we’ve taken from the state, and return it both as the result of the current step, and as the next state07/04 13:06
mietekwe never return Nothing, and so, the result can be unfolded to an arbitrary length07/04 13:06
mietekquchen: does that help?07/04 13:06
quchenmietek: Let me have a look :-D07/04 13:07
quchenHm, I’ve never used codata07/04 13:08
mietekremember the gist I pasted is _pseudocode_07/04 13:08
mietekif you’ve used Haskell, you’ve been using codata all along07/04 13:08
quchen(We met at the Haskell Exchange, remember?) :-)07/04 13:09
quchenI’ve also used mathematics, but since there is no distinction between recursion and corecursion there, being »familiar« isn’t enough :-/07/04 13:10
mietek(sorry, I don’t… 2 years and I haven’t associated a face to the nickname)07/04 13:10
mietekwell, is what I’ve written above unclear in some way?07/04 13:11
mietekI’m happy to try and clarify07/04 13:11
quchencopattern matching doesn’t look very familiar07/04 13:11
quchenIt’s pattern matching inside out, from the looks of it07/04 13:12
mietekhttp://www2.tcs.ifi.lmu.de/~abel/talkIHP14.pdf07/04 13:12
mietekit’s actually an Agda feature07/04 13:12
mietekconstructing a value of a given codatatype T requires providing answers to the questions of, what happens when we observe a value of T in all the allowed ways07/04 13:13
mietekobserve, or deconstruct, or eliminate07/04 13:13
mietekhttp://cs.ioc.ee/~tarmo/tsem12/abel-slides.pdf07/04 13:14
mietekthis is good07/04 13:14
gallaisYeah the key insight with copatterns is the idea you're making observations on a hidden state.07/04 13:21
gallaisWith that in mind you can encode the usual coinductive types (the hidden state is the unfold which created the structure in the first place)07/04 13:21
gallaisBut you can also formalise concepts from other programming languages07/04 13:22
gallaise.g. Abel, Setzer and Adelsberger use it to model object oriented programming07/04 13:22
gallaisor you can formalise some abstract interfaces like iterators: https://github.com/gallais/potpourri/blob/master/agda/poc/Iterator.agda#L1507/04 13:23
quchenmietek: Reminds me a bit of comonads in Haskell07/04 13:25
quchenThose Abel slides are awkward (but good)07/04 13:32
mietekquchen: yes, a (strong) comonad is a structure which allows you to unfold trees of an arbitrary size, right?07/04 13:32
quchenCopatterns look a bit like inverted patterns07/04 13:32
quchenComputation is done in the pattern, it looks like.07/04 13:32
quchenOr we’re pattern matching on a computation07/04 13:32
quchentail (tail fib) = zipWith …07/04 13:32
mieteklook at my gist again07/04 13:32
mietekthe equations I wrote define the computation rules07/04 13:33
quchenYup, I’ve got that open alongside07/04 13:33
mietekgallais: that OOP paper is really good; I just wish they had made the connection to actors and Erlang07/04 13:39
mietekI need to read it in detail07/04 13:39
quchenHm, I tried following the »stream« example, but can’t use the hole :-( http://lpaste.net/296475451069143449607/04 13:40
quchenIt’s from the slides07/04 13:40
mietekcan’t use?07/04 13:40
quchenSplitting on x yields an error07/04 13:40
quchen»A has type Stream .A when checking that the expression ? has type Stream .A07/04 13:41
quchen«07/04 13:41
quchenWait, that’s repeat, not cycle. Anyway, same problem.07/04 13:41
mietekC-r to refine the hole07/04 13:41
mietekyou are *constructing* 07/04 13:42
mietekthe record type would benefit from a constructor07/04 13:42
quchen»cannot refine« :-(07/04 13:42
mietekwhat?07/04 13:42
quchenIsn’t it a co-record?07/04 13:42
mietekcycle x = record { head = {!!} ; tail = {!!} }07/04 13:42
mietekrefines to this 07/04 13:42
quchenOh, I still had the »x« in the hole.07/04 13:42
quchenI’m trying to follow slide 19 here, http://cs.ioc.ee/~tarmo/tsem12/abel-slides.pdf07/04 13:43
mietekah, he does say split07/04 13:44
mietekhe also says "split *result*"07/04 13:44
mietekthat means you do C-c in an empty hole, and hit return07/04 13:44
quchenOooooh. I don’t split the x, I split the entire hole.07/04 13:44
gallaismietek: I don't anything about Erlang so I wouldn't know. Maybe someone needs to write that paper ;)07/04 13:45
mietekquchen: opening the record will help improve notation07/04 13:45
quchenOh noo, copatterns aren’t supported by auto proof search! Do I have to manually type Agda now? Preposterous07/04 13:45
mietekgallais: well, long story short, objects are actors are Erlang processes; method calls are message sends07/04 13:45
mietekquchen: it is unfortunate07/04 13:46
mietekgallais: embedding over inheritance; inheritance is an anti-pattern anyway07/04 13:46
gallaisWe need to rewrite / refactor Auto. Hoping to spend some time on it in May07/04 13:46
quchenCool, http://lpaste.net/176355311550149427207/04 13:46
mietek"open Stream" and you can get rid of "Stream."07/04 13:46
quchenI don’t really understand what I’m doing, but I like it ;-)07/04 13:47
quchenOh, I didn’t know I could open records!07/04 13:47
mietekevery record is also a module07/04 13:47
mietekhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records07/04 13:47
quchenOh, is it just sugar?07/04 13:47
mietekno07/04 13:47
gallaiswell... yes and no. The projections / definitions do live in that parametrised module07/04 13:48
mietekwell, depending on how far you want your definition of sugar to go07/04 13:48
gallaisbut they also have a special status07/04 13:48
mietekgallais: and I am actually working towards that paper07/04 13:49
mietekgallais: slightly different angle on it07/04 13:50
mietekgallais: I think corecursion might actually be the fundamental notion of computation 07/04 13:50
mietekbut that’s best discussed in the other channel :)07/04 13:51
quchenImplementing functions like zip and map is funny. It feels so backwards.07/04 13:52
quchen(Probably because it *is*.)07/04 13:53
quchenWaaait. Why is this valid?07/04 13:53
quchenhead (map f xs) = f (head xs)07/04 13:53
quchentail (map f xs) = map f xs07/04 13:53
quchenThe tail case is clearly nonsense!07/04 13:53
quchenShouldn’t the (co?) termination checker complain?07/04 13:53
quchenOr did I just define a fixed point for the tail?07/04 13:54
gallaisit's fine (except that it doesn't implement `map`, it implement `repeat . f . tail`)07/04 13:54
gallaiss/tail/head07/04 13:55
gallaistry using it with concrete inputs (e.g. f = id, xs = [0..])07/04 13:55
mietekquchen: remember you are describing how to *construct* a thing that may be unfolded to an arbitrary size07/04 13:55
mietekyou gave a description, but it doesn’t do what you originally intended07/04 13:56
mietekbut the intended result may also unfolded to an arbitrary size07/04 13:56
quchenI was just surprised, because »map f (x :: xs) = map f (x :: xs)« isn’t valid, and this looked related07/04 13:56
quchenHm, I see.07/04 13:57
quchenSo the »head« and »tail« functions must be total and terminating07/04 13:57
quchenNot the stream, if that makes sense07/04 13:57
quchenWhereas for lists, the list itself is terminating (finite)07/04 13:57
mieteka value of a given datatype is statically bounded07/04 13:58
mieteka value of a given codatatype may be constructed in a statically bounded way07/04 13:58
mietekhm, to rephrase07/04 13:58
mietekI’m sure Conor had an aphorism on this07/04 13:59
mieteka piece of data promises you can deconstruct it in a finite number of steps, through pattern matching, because a datatype is defined by its constructors07/04 14:00
mieteka piece of codata doesn’t make that promise07/04 14:02
mietekgallais: actually, last slide in http://cs.ioc.ee/~tarmo/tsem12/abel-slides.pdf does say "message passing"!07/04 14:03

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