--- Day changed Thu Jan 11 2018 | ||

Nik05 | I 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 works | 11/01 18:17 |
---|---|---|

Nik05 | data 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 |

pgiarrusso | Nik05: I guess `X \in P A` reduces to `P A X`, solving the mystery | 11/01 19:14 |

pgiarrusso | in 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 normalization | 11/01 19:14 |

pgiarrusso | Nik05: you should check where `\in` is defined to confirm what I’m saying, though my guess is very reasonable | 11/01 19:15 |

pgiarrusso | sets 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 x | 11/01 19:16 |

pgiarrusso | Nik05: as expected | 11/01 19:17 |

pgiarrusso | Nik05: after seeing the definition, can you follow my reasoning? Where do you have questions? | 11/01 19:17 |

Nik05 | Looking at it now, thank you pgiarrusso | 11/01 19:18 |

pgiarrusso | welcome :-) | 11/01 19:18 |

Nik05 | so 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 |

Nik05 | sorry my english | 11/01 19:20 |

Nik05 | Shouldnt 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 U | 11/01 21:30 |

Nik05` | I still don't get it :P | 11/01 21:36 |

pgiarrusso | Nik05: Nik05` the next question is what is S? And U? | 11/01 21:49 |

pgiarrusso | I’m sure reducing those will take you further to the answer | 11/01 21:50 |

Nik05` | S : U -> Set l | 11/01 21:50 |

pgiarrusso | That’s its type... no definition? | 11/01 21:51 |

pgiarrusso | And U? | 11/01 21:51 |

Nik05 | S {u} U = U → Set u | 11/01 21:52 |

Nik05 | thats the definition | 11/01 21:52 |

Nik05 | U is the predicate variable | 11/01 21:52 |

pgiarrusso | It looks like S X means “predicate on X” | 11/01 21:52 |

Nik05` | Yes | 11/01 21:54 |

Nik05` | Or is this a strange definition? | 11/01 21:54 |

pgiarrusso | And since S (S X) means U -> S X, the mismatch indeed disappears | 11/01 21:55 |

pgiarrusso | It’s not so strange, it’s pretty standard | 11/01 21:55 |

pgiarrusso | But if you have more questions, it might be easier if you sent a complete example | 11/01 21:56 |

pgiarrusso | Though maybe we’re (almost) done | 11/01 21:56 |

Nik05` | Oke | 11/01 21:56 |

pgiarrusso | Nik05`: generally, the typechecker must run definitions before comparing types, and you must do the same (as we’ve done) to follow what it does | 11/01 21:57 |

pgiarrusso | It seems that P A should be something like the powerset of A? | 11/01 21:58 |

Nik05` | Yes indeed | 11/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 Set | 11/01 22:03 |

Nik05` | Or | 11/01 22:04 |

Nik05` | Wait | 11/01 22:04 |

Nik05 | it is | 11/01 22:07 |

Nik05 | pgiarrusso when i make a hole in the last return type and fill in my definition agda doesnt except the definition... | 11/01 22:19 |

Nik05 | oh maybe this is a constraint problem | 11/01 22:20 |

pgiarrusso | You’ll need to add back the Set levels to inline the definition by hand | 11/01 22:21 |

pgiarrusso | Or maybe it’s some other such stupid detail going wrong, but guessing from here is hard | 11/01 22:21 |

Nik05 | '_152 : S U' this is my constraint error | 11/01 22:22 |

Nik05 | no idea how to read that | 11/01 22:22 |

pgiarrusso | Not a complete error message; but that underscore thing is a metavariable, so it’s somehow failing to infer some implicit parameter | 11/01 22:28 |

pgiarrusso | Nik05: again, hard to help without actual code + error, you should use a self-contained gist | 11/01 22:28 |

pgiarrusso | Meanwhile, time to go to bed for me | 11/01 22:29 |

Nik05 | have a good night pgiarrusso | 11/01 22:29 |

Nik05 | thank you a lot | 11/01 22:29 |

pgiarrusso | Nik05: good night! | 11/01 22:29 |

Nik05 | thank you | 11/01 22:29 |

Nik05 | next time i will, sorry thought i would get this simple problem | 11/01 22:30 |

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