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

--- Day changed Mon Mar 27 2017
vorgangwedify: thanks, it was using /usr/bin/agda, not the cabal version. Deleted that, it works now. There's seems to be no stdlib though....27/03 04:11
vorgangDoes the cabal package "Agda" also include stdlib?27/03 05:38
wedifyvorgang: no it does not27/03 08:58
wedifyeasy to set it up though27/03 09:00
Saizanmietek: it's in "i have to document it" status, so actually more users would be nice27/03 10:13
Saizanmietek: it's merged in master27/03 10:13
mietekSaizan: cool. 27/03 10:13
mietek{AS}: ^^27/03 10:13
{AS}ah cool27/03 10:13
mietekI’m having trouble locating Catarina Coquand’s webpage…27/03 10:14
mietekAnyone?27/03 10:15
{AS}mietek: link27/03 10:16
mietek{AS}: I can’t find a link; that’s the thing27/03 10:17
{AS}ah27/03 10:17
{AS}I think I thought you meant accessing27/03 10:17
mietekThat’s very self-reflective of you27/03 10:18
{AS}mietek why do you need her webpage?27/03 10:21
mietekI want to ask if she still has the full Alf code accompanying her 2002 paper27/03 10:21
{AS}I can't find it27/03 10:21
{AS}Ah27/03 10:21
{AS}you can just use the registry of Chalmers no?27/03 10:21
mietekhttp://www.hh.se/omwebbplatsen/sokpawebbplatsen/personalkatalog.2637.html?url=-1708965309%2Fl9%2Fhhstaff%2Fen%2Fdetail.lasso%3Fdo%3Dstart%26groupmember%3D35AA3CED-44BF-4833-A72E-B8AA19AF7850&sv.url=12.2a98b8e2153dde2b50b9556927/03 10:21
mietekThis seems to be current27/03 10:22
{AS}yeah27/03 10:24
{AS}I see27/03 11:53
{AS}err, wrong channel27/03 11:53
vorgangwedify: but how? I can't find a cabal package for Agda stdlib27/03 18:27
glguyThe Agda std-lib isn't a Haskell library, it's an Agda library; there's no cabal package for it27/03 18:29
glguyvorgang: Here's how I've got it setup : http://lpaste.net/521192855869954457627/03 18:34
dolioDo you run Agda from the git repo? I tried updating everything (library and binary) the other day, but the compiler didn't like something in the library.27/03 18:37
glguyI do, but I think it has tags to get particular version27/03 18:40
dolioI installed Agda from hackage, so maybe it's too old.27/03 18:40
glguyYeah, you might have to roll back to an older tag for hackage27/03 18:41
glguyI appear to have "Agda version 2.5.2" and agda-stdlib commit a79f1fb7d78d4f5e042dcf553f8156ed85a146be specifically27/03 18:41
vorgangglguy: So Agda knows about ~/.agda/libraries and ~/.agda/defaults ?27/03 20:05
vorgangglguy: it kind of works now... at least I get a different error27/03 20:26
vorgangglguy: did you also compile agda-stdlib, or just pull the repo?27/03 20:28
sleffyI've found myself needing a universe-polymorphic bottom type. Is this reasonable in any way shape or form? Or should I reevaluate my terrible decisions?27/03 20:37
mieteksleffy: ⊥ itself, or ⊥-elim?27/03 20:42
sleffymietek, \bot itself.27/03 20:42
mietekcan you give an example of how this happens?27/03 20:42
sleffyI have a feeling this is due to my naivete27/03 20:42
dolioI could imagine some places where it might come up.27/03 20:43
sleffymietek: https://pastebin.com/raw/450TBKHZ27/03 20:44
sleffyI have cases where I have a `Maybe A` where `A` is not in `Set 0`. In that case, `NoConfusion-Maybe` has to put out an equality which is in `Set l`, where `l` is whatever level `A` is in27/03 20:45
mietekI’m quite confused27/03 20:45
sleffyYeah, that's not a big surprise. I don't really know what I'm doing27/03 20:45
sleffyWhat I wanted to do was be able to take any equality of the form `just x = nothing` or `nothing = just x`, and produce bottom27/03 20:45
mietekare you trying to write a decidable equality?27/03 20:45
sleffyNo27/03 20:45
sleffyI'm trying to prove that a partial function always produces `just x` when given a particular sort of proof on its inputs27/03 20:46
sleffyIn the process, I end up with a lot of inequalities of the form `just x = nothing` or `nothing = just x`27/03 20:46
mietekwell : ∀ {ℓ} {X : Set ℓ} {x : X} → just x ≡ nothing → ⊥27/03 20:46
mietekwell ()27/03 20:46
sleffySo I wanted a tool to better deal with discharging them27/03 20:47
sleffyI saw someone's NoConfusion implementation for I forget what type on the internet and then tried to imitate it :P27/03 20:47
sleffymietek, that's what I was originally going to do but I also end up with the other way around, and I was hoping to use the same lemma for both27/03 20:47
mietekllew : ∀ {ℓ} {X : Set ℓ} {x : X} → nothing ≡ just x → ⊥27/03 20:48
mietekllew = well ∘ sym27/03 20:48
sleffyWell, I'll run with that for now then. As an aside, how do you type the cursive l?27/03 20:49
mietek\ell27/03 20:49
sleffythx :)27/03 20:49
mietekwelcome27/03 20:49
mietekalso, c-U c-X = should tell you how to type any character you have highlighted in emacs27/03 20:50
mieteklook for the 'to input:' line27/03 20:50
sleffyThat's really useful! Thanks again.27/03 20:51
sleffymietek, as an aside: on the `well` and `llew` definitions, Agda can't seem to infer the implicits on the `just x ≡ nothing`. I get a lot of "failed to solve constraints" errors.27/03 20:57
sleffyIf I rewrite the type signature to `well : ∀ {ℓ} {X : Set ℓ} {x : X} → just x ⟨ _≡_ {ℓ} {Maybe X} ⟩ nothing → ⊥`, then it works out, but it's a bit ugly. Is there a better way to give Agda the missing info?27/03 20:57
mietektry `Maybe.just`27/03 20:57
mietekthe problem is name overloading in the stdlib27/03 20:57
mietekI use my own micro-prelude nowadays27/03 20:57
sleffyoh, huh. That did the trick. Thanks again!27/03 20:58
mietekthere are simply multiple `just` constructors in Data.Maybe27/03 21:00
mietekwhich is a bit weird27/03 21:00
glguyvorgang: I think I just pulled the repo. There might be elements that need to be compiled for uses I haven't tried27/03 21:02
christiansenthe Agda docs say that old-style coinduction with ∞ is inconsistent, but Google is not helping me find a counterexample. anyone know off the top of their heads?27/03 22:21
{AS}christiansen: https://github.com/agda/agda/issues/1209 maybe ?27/03 22:27
{AS}christiansen: https://github.com/agda/agda/issues/1209#issuecomment-129029487 <- sorry27/03 22:27
christiansen{AS}: thanks27/03 22:28
{AS}np27/03 22:28
{AS}If you are trying to do your own coinduction I can recommend guarded recursive types :)27/03 22:29
christiansen{AS}: I'm hunting Idris bugs, and old/fixed/wontfixed Agda bugs are a good source27/03 22:29
christiansenbest to learn from those who have come before :)27/03 22:29
{AS}christiansen: Ah cool27/03 22:29
{AS}I can still recommend guarded recursive types, but I guess we would need someone to implement them27/03 22:29
christiansenyou mean like the ones Rasmus & the Aarhus folks work on, right?27/03 22:30
{AS}Yeah27/03 22:31
{AS}You would probably also need cubical (AFAIR) to get equality working rightly27/03 22:31
{AS}so I guess maybe after 1.027/03 22:32
christiansenOTT should work as well, I'd think - the key is getting canonicity + the right prop. eq. for codata, right?27/03 22:32
{AS}christiansen: Hmm, yeah. It's because codata equality should be extensional27/03 22:33
{AS}so if you care more about UIP than Path induction then OTT should work27/03 22:33
* {AS} just wanted an excuse to get cubical into Idris :)27/03 22:35
christiansen{AS}: K is baked in pretty solidly - it'd be a lot of work. I think Cubical Agda will be ready for play much sooner!27/03 22:35
{AS}I was recently told that cubical Agda is ready :)27/03 22:36
christiansenoh, great news!27/03 22:37
* christiansen is behind on things27/03 22:37
jonsterlingYes, i've heard it basically works except for "with expressions"! Haven't gotten around to playing with it yet27/03 23:16
jonsterlingJust finished up jrw's patch to support hypothetical judgments in user-level theorem declarations!27/03 23:56
jonsterlinghttps://usercontent.irccloud-cdn.com/file/X3Zlc7mk/Screen%20Shot%202017-03-27%20at%206.55.11%20PM.png27/03 23:57
jonsterlingThis is the first step, I suppose, toward supporting MetaPRL-style sequent schemata.27/03 23:57
jonsterlingSuper excited about this.27/03 23:57
jonsterlingOops, I put this in the wrong channel. Sorry about that!27/03 23:57

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