--- Day changed Thu Jan 11 2018
Nik05I got a question about inductive types, I thought all sub function types need to end with the inductive type. But I got a inductive type that im not sure how it works11/01 18:17
Nik05data P {u} {U : Set u} (A : S U) : S (S U) where P≙ : ∀ {X : S U} → X ⊆ A → X ∈ (P A)11/01 18:18
pgiarrussoNik05: I guess `X \in P A` reduces to `P A X`, solving the mystery11/01 19:14
pgiarrussoin general the “sub function types” must indeed end with the inductive types — or better, the constructors must indeed construct the inductive, but that’s tested after normalization11/01 19:14
pgiarrussoNik05: you should check where `\in` is defined to confirm what I’m saying, though my guess is very reasonable11/01 19:15
pgiarrussosets can be seen as predicates (the characteristic function of the set), and then `s \in S` (element `s` belongs to set `S`) becomes `S s` (element `s` satisfies predicate `S`)11/01 19:16
Nik05`x in A is defined as A x11/01 19:16
pgiarrussoNik05: as expected11/01 19:17
pgiarrussoNik05: after seeing the definition, can you follow my reasoning? Where do you have questions?11/01 19:17
Nik05Looking at it now, thank you pgiarrusso 11/01 19:18
pgiarrussowelcome :-)11/01 19:18
Nik05so X in P A indeed reduces to P A X, but shouldnt the function and in P A and not in P A X?11/01 19:19
Nik05sorry my english11/01 19:20
Nik05Shouldnt the function end in 'P A' and not in 'P A X'?11/01 19:20
Nik05`pgiarrusso: sorry but my inductive type is P : A -> S (S U). But the last type is P A X : S U11/01 21:30
Nik05`I still don't get it :P11/01 21:36
pgiarrussoNik05: Nik05` the next question is what is S? And U?11/01 21:49
pgiarrussoI’m sure reducing those will take you further to the answer11/01 21:50
Nik05`S : U -> Set l11/01 21:50
pgiarrussoThat’s its type... no definition?11/01 21:51
pgiarrussoAnd U?11/01 21:51
Nik05S {u} U = U → Set u11/01 21:52
Nik05thats the definition11/01 21:52
Nik05U is the predicate variable11/01 21:52
pgiarrussoIt looks like S X means “predicate on X”11/01 21:52
Nik05`Yes11/01 21:54
Nik05`Or is this a strange definition?11/01 21:54
pgiarrussoAnd since S (S X) means U -> S X, the mismatch indeed disappears11/01 21:55
pgiarrussoIt’s not so strange, it’s pretty standard11/01 21:55
pgiarrussoBut if you have more questions, it might be easier if you sent a complete example11/01 21:56
pgiarrussoThough maybe we’re (almost) done11/01 21:56
Nik05`Oke11/01 21:56
pgiarrussoNik05`: generally, the typechecker must run definitions before comparing types, and you must do the same (as we’ve done) to follow what it does11/01 21:57
pgiarrussoIt seems that P A should be something like the powerset of A?11/01 21:58
Nik05`Yes indeed11/01 22:00
Nik05`I still don't see how it matches. P A has type S (S U) = (U -> Set) -> Set. P A X has type Set11/01 22:03
Nik05`Or11/01 22:04
Nik05`Wait11/01 22:04
Nik05it is11/01 22:07
Nik05pgiarrusso when i make a hole in the last return type and fill in my definition agda doesnt except the definition...11/01 22:19
Nik05oh maybe this is a constraint problem11/01 22:20
pgiarrussoYou’ll need to add back the Set levels to inline the definition by hand11/01 22:21
pgiarrussoOr maybe it’s some other such stupid detail going wrong, but guessing from here is hard11/01 22:21
Nik05'_152 : S U' this is my constraint error11/01 22:22
Nik05no idea how to read that11/01 22:22
pgiarrussoNot a complete error message; but that underscore thing is a metavariable, so it’s somehow failing to infer some implicit parameter11/01 22:28
pgiarrussoNik05: again, hard to help without actual code + error, you should use a self-contained gist11/01 22:28
pgiarrussoMeanwhile, time to go to bed for me11/01 22:29
Nik05have a good night pgiarrusso 11/01 22:29
Nik05thank you a lot11/01 22:29
pgiarrussoNik05: good night!11/01 22:29
Nik05thank you11/01 22:29
Nik05next time i will, sorry thought i would get this simple problem11/01 22:30

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