--- Day changed Tue Feb 07 2017
rntzhttp://sprunge.us/PQeX I'm running into the strict positivity constraint in agda - anyone have suggestions for ways around this?07/02 00:30
rntz(it complains about _|-_ not being strictly positive)07/02 00:31
rntzhm, it looks like just changing args to a datatype rather than a function producing a type works...07/02 00:33
rntzoh, or even just rewriting it to be more explicitly recursive07/02 00:34
rntzer, inductive07/02 00:34
akrIf I want to define polynomials over some algebraic structure, e.g. a group, how do I do it? As an inductive data type, defined separately from the record giving the definition of a group?07/02 15:24
akrOr can I somehow include it in the record and reuse my already existing fields for _⋅_, etc.?07/02 15:25
akrnevermind07/02 15:36
akr⊨ ϕ = ∀ {{_ : ModalAlgebra}} → {!⊨ᵛ ϕ!}07/02 16:16
akrNo instance of type ModalAlgebra was found in scope.07/02 16:17
akrwhat07/02 16:17
akrI want to do something like this: https://mietek.github.io/hilbert-gentzen/html/BasicIPC.Semantics.KripkeConcrete.html#60407/02 18:38
akrbut my record is parametrized07/02 18:38
akrand for some reason, when I attempt this (e.g. 'module _ {{Label : Set}} {{M : ModalAlgebra Label}} where …'), every usage of a projection from the record becomes unresolvable07/02 18:39
akrhttps://i.imgur.com/wW8IS0t.png07/02 18:41
akris there some sensible way to solve this?07/02 18:41
pgiarrussoakr: since a while, Agda only solves instances when their type has no open metavariables.07/02 18:42
akroh07/02 18:42
pgiarrussoin older Agdas, you would have had a chance with Label as an implicit, not instance argument.07/02 18:43
pgiarrusso*however*07/02 18:43
pgiarrussocan you turn Label into a member of ModalAlgebra?07/02 18:43
pgiarrussoor have a variant of ModalAlgebra having that as a member? it seems that could solve the problem :-)07/02 18:43
pgiarrusso(the usual pattern in Agda stdlib for instances is to have IsModalAlgebra member1 member2 member3 and then ModalAlgebra with all members as members and not params)07/02 18:44
pgiarrussoakr: does that help?07/02 18:44
akrthat was my original solution, but this is problematic in another function, it would look like this:07/02 18:46
akr⊨_ : ∀ {Label : Set} → (K.Form Label) → Set₁07/02 18:46
akr⊨ ϕ = ∀ {{M : ModalAlgebra}} → {!!}07/02 18:46
akrhere I would want to ensure that the Label is the same as Label inside the ModalAlgebra M07/02 18:47
akrI suppose I could to that with propositional equality, like ⊨ {Label} ϕ = ∀ {{M : ModalAlgebra}} → Label ≡ (ModalAlgebra.Label M) →  {!!}07/02 18:47
akrbut it's not very nice07/02 18:48
pgiarrussoakr: yeah, that’s one reason why you also need IsModalAlgebra — which might even work there?07/02 18:50
akrhmm okay I'll give that a try, I don't see how exactly it would work yet07/02 18:51
pgiarrussoakr: yeah, if K.Form is a constructor (as opposed to a function), unification can infer Label from the argument ϕ07/02 18:51
akrah, cool07/02 18:52
pgiarrussonot sure whether that helps for calling the function, but it might07/02 18:52
akrK.Form is a parametrized data type07/02 18:52
pgiarrussogood07/02 18:52
pgiarrussoakr: you familiar with Hindley-Milner inference/unification?07/02 18:52
akrnot in any great detail07/02 18:53
pgiarrussoYeah, the point about why K.Form should be a datatype for this to work? Familiarity with that would help to have intuition for that point07/02 18:54
pgiarrussoOTOH, Agda typechecking is *not* HM even if it does use unification07/02 18:54
pgiarrussosorry about that07/02 18:55
pgiarrussoakr: anyway, at least I’m confident if you call f : ∀ {Label : Set} → (K.Form Label) ->  {{M : IsModalAlgebra Label}} -> ?, with a K.Form Label, Label can be inferred from that and then the M argument should be inferrable (at least, it doesn’t have open metas)07/02 18:55
akrhmm, but in my case IsModalAlgebra would be in the definition, not in the type07/02 18:57
pgiarrussoakr: yeah, I realize that’s different, which is why I clarified… it might help at the call sites or not (possibly depending on the call sites).07/02 19:00
akrso just to be clear, what I would do would have to be something like, ⊨ {Label} ϕ = ∀ {{M : IsModalAlgebra Label C _∧_ …}} → let M' = ModalAlgebra {Label C _∧_ … M} in ?07/02 19:04
pgiarrussoakr: uh, wasn’t thinking about the let07/02 19:06
pgiarrussoin the stdlib the ModalAlgebra does an open public of the IsModalAlgebra so you can use the same field accessors and contained functions07/02 19:06
pgiarrussoI don’t know if you can make a copy of ModalAlgebra into an instance07/02 19:07
akrI was thinking that I would use the parametrized IsModalAlgebra to get a ModalAlgebra of the correct sort (which is given by the argument Label)07/02 19:09
pgiarrussoakr: sure sure, and that’s fine, just wondering if that overhead can be reduced07/02 19:11
akrideally, there would be some sort of function to which I would give the argument Label : Set, and it would return the type of ModalAlgebra where ModalAlgebra.Label has been fixed to that argument07/02 19:13
akrbut I don't suppose that's doable07/02 19:13
akrmaybe I should make the whole module parametrized by Label and be done with it07/02 19:26
mietekakr: there’s annoying bugs with parametrized modules07/02 21:03
pgiarrussomietek: at least they fixed the crashes in #1985 :-)07/02 21:36

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