--- Day changed Fri Mar 24 2017 | ||

akr[m] | glguy: I know, I was just thinking that this bight be more elegant with the use of sized types :) | 24/03 07:22 |
---|---|---|

akr[m] | I mean, I could just use ℕ as the size I think | 24/03 07:25 |

arjen-jonathan | Hi all | 24/03 13:00 |

arjen-jonathan | I broke agda again | 24/03 13:01 |

arjen-jonathan | :( | 24/03 13:01 |

arjen-jonathan | Also, the gmain link in the title is dead | 24/03 13:02 |

Saizan | arjen-jonathan: i.e. you proved false? | 24/03 13:06 |

arjen-jonathan | No, it's not *that* broken | 24/03 13:08 |

arjen-jonathan | Typechecker loops | 24/03 13:08 |

arjen-jonathan | It seems | 24/03 13:08 |

arjen-jonathan | You're working on parametricity? | 24/03 13:11 |

Saizan | yep | 24/03 13:14 |

arjen-jonathan | That's awesome. How's it going? | 24/03 13:16 |

Saizan | so far it can be used for some irrelevance properties, but general "free theorems" are a bit limited by how we cannot have parametricity proofs about parametricity proofs | 24/03 13:19 |

Saizan | it's been challenging to find the right denotational model | 24/03 13:19 |

Saizan | and we might have to modify it again | 24/03 13:20 |

arjen-jonathan | Are you publishing on this topic? | 24/03 13:24 |

Saizan | we have a draft, pm me an address and I can mail it to you | 24/03 13:25 |

dolio | akr[m]: I think I'm wrong, and Saizan is right. Nat is isomorphic to coNat in the classical set model. But that isomorphism can't be continuous with respect to the 'computability topology.' | 24/03 14:35 |

akr[m] | I'm not sure what that means; to me it seems that the classical isomorphism is not a computable function | 24/03 14:37 |

dolio | Yes, that's what it means. | 24/03 14:37 |

dolio | There are some fixed points where least coinciding with greatest will provably not work. | 24/03 14:39 |

dolio | Like, fixed point of identity. | 24/03 14:39 |

dolio | Least is empty set, greatest is singleton set. | 24/03 14:39 |

akr[m] | I'm not sure what's our function space when talking about fixed points here | 24/03 14:41 |

dolio | Something like covariant functors. | 24/03 14:44 |

dolio | At least for sets. | 24/03 14:45 |

Saizan | yeah, it feels weird, but in the end it's just that they are both countable sets | 24/03 14:51 |

dolio | Well, I wasn't exactly sure that it wouldn't end up bigger than that. | 24/03 15:05 |

dolio | Because I think there could be some sets in the classical set model that aren't countable. | 24/03 15:05 |

dolio | The question is whether you could somehow use those to construct 'longer' stepping sequences or something. | 24/03 15:06 |

dolio | And not just produce them, but produce enough that there are uncountably many things in the final coalgebra. | 24/03 15:07 |

Saizan | is there an easy way to characterize which functors have isomorphic initial/final (co)algebras? | 24/03 15:40 |

Saizan | maybe all finitary-branching functors have isomorphic initial/final (co)algebras if those are both infinite | 24/03 15:40 |

Saizan | because it only takes induction over omega to build both | 24/03 15:40 |

dolio | How branching is id? | 24/03 15:41 |

Saizan | the initial algebra of id is not infinite :) | 24/03 15:42 |

dolio | Oh, if infinite. | 24/03 15:42 |

dolio | I don't think that works. | 24/03 15:44 |

dolio | Like, finite bit sequences is not going to be isomorphic to potentially infinite bit sequences, classically. | 24/03 15:44 |

dolio | There are too many of the latter, right? | 24/03 15:44 |

dolio | Uncountably many infinite ones. | 24/03 15:45 |

Saizan | uh, right | 24/03 15:46 |

Saizan | ok, now i'm also more surprised by conat being countable | 24/03 15:48 |

dolio | Well, the difference there is that the uncountable bit sequences all have the same length. | 24/03 15:48 |

dolio | But they have different content. | 24/03 15:48 |

dolio | But (co)naturals have no content other than length. | 24/03 15:49 |

Saizan | makes sense, everything that makes that set big is actually collapsed into the "infinity" element in (co)naturals | 24/03 15:51 |

dolio | Right. The uncountably many things get quotiented down to a single thing. :) | 24/03 15:51 |

dolio | Although I don't have a good explanation for why you can't have different infinite lengths of things. | 24/03 15:52 |

dolio | Other than that bisimulation is defined in terms of the naturals. | 24/03 15:53 |

dolio | Instead of some more general thing. | 24/03 15:53 |

dolio | Like how mathematicians move from natural-indexed sequences to filters for some things in topology, because the former is limiting. | 24/03 15:54 |

dolio | Or how 'directed sets' are more general than omega chains. | 24/03 15:55 |

Saizan | my rough understanding is that it depends on the functor, but a lot of them commute with limits over the naturals, so longer chains would still reach the same fixed point | 24/03 15:58 |

dolio | Ah. | 24/03 15:58 |

akr[m] | Given a list of values, I want to construct the type of these values | 24/03 16:37 |

akr[m] | is there something better I can do than dependent products? | 24/03 16:37 |

akr[m] | (avoiding metaprogramming) | 24/03 16:37 |

akr[m] | maybe avoiding lists altogether, hmm | 24/03 16:39 |

akr[m] | my situation is like this: http://lpaste.net/353895 | 24/03 16:44 |

akr[m] | Atomic is something which is defined by the type of states it can be in | 24/03 16:44 |

akr[m] | Struct is determined by the Atomics it is made up of | 24/03 16:44 |

akr[m] | and I'd like to have something like Signature, which is the type of atomics some given struct is made of | 24/03 16:45 |

mietek | Saizan: what’s the status of Agda/cubical? https://github.com/agda/agda/issues/1703 | 24/03 22:30 |

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