--- Day changed Mon Nov 23 2015
Ralithtypes have be said to have structure in many ways23/11 00:01
Ralithcan you be more specific23/11 00:01
Ralithcan be said*23/11 00:01
R0b0t1... no, because you can construct a pattern in many ways.23/11 00:04
R0b0t1because it could be considered to be a type23/11 00:04
R0b0t1or have a type23/11 00:04
RalithR0b0t1: isn't a pattern just a variable, a constructor fully applied to some patterns, or an inaccessible term?23/11 00:54
R0b0t1Ralith: no23/11 01:35
R0b0t1Ralith: https://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf23/11 01:35
R0b0t1it is a syntactic structure23/11 01:35
R0b0t1that exists outside of the concepts of contexts and types23/11 01:36
RalithR0b0t1: so why were you saying they were types? o.O23/11 02:34
R0b0t1<R0b0t1> because it could be considered to be a type23/11 02:43
R0b0t1it describes one23/11 02:43
int-indexHi.23/11 09:07
int-indexIs there a way to shorten decidable equality definition using reflection? I'm dealing with a simple type, so the definition is mostly boilerplate: https://github.com/int-index/foundry-agda/blob/master/Foundry/Node.agda#L11123/11 09:08
tomjackint-index: here's a first attempt: http://s3.tomjack.co/2e59994a-fd3d-4b7c-a39a-fcc18ce766dd/Enum.html23/11 12:56
tomjackmodified this from a version I had sitting around that was fully automated for non-indexed enums. the problem is that using pattern lambdas here only seems to work if you handle the different index cases separately, but then you need to automatically figure out which constructors go in which case, and automate handling the cases23/11 12:59
int-indextomjack: turns out it's not as simple as I thought!23/11 13:06
int-indexThank you for the code, I'll see what I can do with it23/11 13:18
int-indexI believe that instead of generating terms it's possible to generate complete definitions.23/11 13:22
tomjackas far as I know, pat-lam is the only way to generate pattern matching code. but you should be able to generate a pat-lam which also pattern matches on the implicit index args23/11 16:08
Saizani wish we could keep track of situations like f : (a : A) -> P a -> Q a,  "subst Q eq (f a p)" so that they could get normalized to "f b (subst P eq p)" 23/11 18:42
R0b0t1oh so you can't do that23/11 19:07
R0b0t1https://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf23/11 19:08
R0b0t1int-index: ^ ?23/11 19:08
R0b0t1I mean that probably doesn't do you any good even if it's what you're after23/11 19:08
int-indexthat's what Richard Eisenberg is doing at the moment, I track his progress on GitHub and can't wait when it lands in GHC23/11 19:10
int-indexThis will make it possible to achieve what I want in Haskell, but it's still going to be ugly (lots of singletons)23/11 19:11
int-indexThat is, until Haskell gets proper pi-types23/11 19:13
R0b0t1yeah23/11 19:13
R0b0t1I went to implement it because I wanted to play with similar type systems, but got sidetracked for 2-3 days reading about graph problem optimization23/11 19:16
R0b0t1so uh23/11 19:16
* R0b0t1 sighs23/11 19:16
R0b0t1Saizan: what you want to do is possible with a few exceptions23/11 19:17
R0b0t1welp I don't have a concise explanation, back later23/11 19:18
SaizanR0b0t1: what do you mean? i can prove those two are propositionally equal, getting one to compute to the other would be nicer though23/11 19:21
R0b0t1Saizan: depending on what constraints you give a type and your type system it's possible to enumerate every possible type that could be put there, and turn it into any other type that could be put there23/11 19:27
R0b0t1so you could write the first one somewhere, but then write the second one somewhere23/11 19:27
R0b0t1unless you meant something different by normalized than I expected23/11 19:28
R0b0t1what's interesting is not only can one create type systems where the types generate a regular language, it's possible to handle some cases of nontrivial recursion as well (and still prove termination)23/11 19:30
--- Log closed Mon Nov 23 19:39:00 2015
--- Log opened Mon Nov 23 19:40:13 2015
-!- Irssi: #agda: Total of 101 nicks [0 ops, 0 halfops, 0 voices, 101 normal]23/11 19:40
Saizani don't understand what you are getting at with the rest of what you are saying, but i'm pretty sure i don't want to enumerate things23/11 19:40
-!- Irssi: Join to #agda was synced in 130 secs23/11 19:42
R0b0t1you don't, it's done for you23/11 19:42
R0b0t1yeah this is what I was talking about when I said I couldn't think of a concise explanation23/11 19:43
R0b0t1it'll probably sound like nonsense until I'd have explained the whole thing23/11 19:43
R0b0t1Saizan: https://github.com/int-index/foundry-agda/blob/master/Foundry/Node.agda#L111 that bit happens magically, and it can happen more than most people think it can happen23/11 19:44
Saizanwhich bit do you mean? the case split?23/11 19:46
R0b0t1the list of equalities23/11 19:48
Saizanbtw you can assume i know agda pretty well in your explanation, i've been using it for 7 years23/11 19:48
R0b0t1I was going to say something about not meaning to be condescending but23/11 19:48
R0b0t1it's more I can't explain it23/11 19:48
R0b0t1not that I think you can't understand it23/11 19:48
R0b0t1basically you "factor" your program using a dynamic programming method23/11 20:00
R0b0t1and then you end up with a list of orthogonal types you try to reduce everything to23/11 20:01
R0b0t1which you can use to create equivalence relations23/11 20:02

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