On Fri, Aug 31, 2012 at 9:06 AM, Edward Kmett
I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful.
To flesh this out slightly, there are two options for defining pairs in Agda: data Pair1 (A B : Set) : Set where _,_ : A -> B -> Pair1 A B record Pair2 (A B : Set) : Set where constructor _,_ field fst : A snd : B Now, if we have something similar to Thrist indexed by Pair2, we have no problems, because: A p -> M A p is equal to: A (fst p , snd p) -> M A (fst p , snd p) Which is what we need for the irt definition to make sense. If we index by Pair1, this won't happen automatically, but we have an alternate definition of irt: irt : {I J : Set} {A : Pair1 I J -> Set} {p : Pair1 I J} -> A p -> Thrist A p irt {I} {J} {A} {i , j} ap = ap :- Nil The pattern match {i , j} there refines p to be (i , j) everywhere, so the definition is justified. Without one of these two options, these definitions seem like they're going to be cumbersome. Ed seems to have found a way to do it, by what looks kind of like hand implementing the record version, but it looks unpleasant. On another note, it confuses me that m -> k would be necessary at all in the IMonad definition. k is automatically determined by being part of the kind of m, and filling in anything else for k would be a type error, no? It is the same kind of reasoning that goes on in determining what 'a' is for 'id :: forall a. a -> a' based on the type of the first argument. -- Dan