Thanks, this makes it a lot clearer, it just leaves two questions open: Is there a better way to conjure up polykinded unification/type variables (bonus points if they are not called `k0` and `k1` afterwards)?
Why are some type families flattened and some are not (for the last argument of `RowExt` `RNil` is not evaluated, but another `RowExt` is)? Thanks for your help, I will definitely add a new Note there. Cheers, Jan Am 28.08.19 um 09:52 schrieb Simon Peyton Jones: > Thanks Iavor for your reply -- all correct I think. Re > > | This is the basic idea, but axioms are encoded in a slightly different > | way---instead of being parameterized by just types, they are > | parameterized by equalities (the reason for this is what I seem to have > | forgotten, or perhaps it changed). > > you'll find the reason documented in TyCoRep > Note [Coercion axioms applied to coercions] > > There are other useful Notes in that file about axioms. > > Jan: if you would care to document some of this in a way that makes sense to > you, you could add a new Note. That would help everyone! > > Simon > > > | -----Original Message----- > | From: ghc-devs <[email protected]> On Behalf Of Iavor Diatchki > | Sent: 28 August 2019 01:12 > | To: Jan van Brügge <[email protected]> > | Cc: [email protected] > | Subject: Re: A few questions about BuiltInSynFamily/CoAxiomRules > | > | Hello Jan, > | > | I think I added these sometime ago, and here is what I recall: > | > | * `sfInteractTop` and `sfInteractInert` are to help with type inference: > | they generate new "derived" constraints, which are used by GHC to > | instantiate unification variables. > | - `sfInteractTop` is for facts you can get just by looking at a > | single constraint. For example, if we see `(x + 5) ~ 8` we can generate a > | new derived constraint `x ~ 3` > | - `sfInteractIntert` is for facts that you can get by looking at > | two constraints together. For example, if we see `(x + a ~ z, x + b ~ x)` > | we can generate new derived constraint `a ~ b`. > | - since "derived" constraint do not need evidence, these are just > | equations. > | > | * `sfMatchFun` is used to evaluate built-in type families. For example > | if we see `5 + 3`, we'd like ghc to reduce this to `8`. > | - you are correct that the input list are the arguments (e.g., > | `[5,3]`) > | - the result is `Just` if we can perform an evaluation step, and the > | 3-tuple contains: > | 1. the axiom rule to be used in the evidence (e.g. "AddDef") > | 2. indexes for the axiom rule (e.g.,"[5,3]") (see below for more > | info) > | 3. the result of evaluation (e.g., "8") > | > | Part 2 is probably the most confusing, and I think it might have changed a > | bit since I did it, or perhaps I just forgot some of the details. Either > | way, this is best explained with > | an example. The question is "What should be the evidence for `3 + 5 ~ > | 8`?". > | > | In ordinary math one could do a proof by induction, but we don't really > | represent numbers in the unary notation and we don't have a way to > | represent inductive proofs in GHC, so instead we decided to have an > | indexed family of axioms, kind of like this: > | > | * AddDef(3,5) : `(3 + 5) ~ 8` > | * AddDef(2,1) : `(2 + 1) ~ 3` > | * ... > | > | So the types in the second element of the tuple are these indexes that > | tell you how to instantiate the rule. > | > | This is the basic idea, but axioms are encoded in a slightly different > | way---instead of being parameterized by just types, they are > | parameterized by equalities (the reason for this is what I seem to have > | forgotten, or perhaps it changed). > | So the `CoAxiomRules` actually look like this: > | > | * AddDef: (x ~ 3, y ~ 5) => (x + y ~ 8) > | > | When we evaluate we always seem to be passing trivial (i.e., "refl") > | equalities constructed using the second entry in the tuple. For example, > | if `sfMathcFun` returns `Just (axiom, [t1,t2], result)`, then the result > | will be `result`, and the evidence that `MyFun args ~ result` will be > | `axiom (refl @ t1, refl @ t2)` > | > | You can see the actual code for this if you look for `sfMatchFun` in > | `types/FamInstEnv.hs`. > | > | I hope this makes sense, but please ask away if it is unclear. And, of > | course, it would be great to document this properly. > | > | -Iavor > | > | > | > | > | > | > | > | > | > | > | > | > | > | > | > | > | > | On Tue, Aug 27, 2019 at 3:57 PM Jan van Brügge <[email protected]> wrote: > | > > | > Hi lovely people, > | > > | > sorry if my recent emails are getting annoying. > | > > | > In the last few days I refactored my code to use `BuiltInSynFamily` > | > and `CoAxiomRule` to replace what was very ad-hoc code. So far so > | > easy. But I have a few questions due to sparse documentation. > | > > | > First, about `BuiltInSynFamily`. It is a record of three functions. > | > From what I can tell by looking at `TcTypeNats`, the two `interact` > | > functions are used to solve the argument parts of builtin families > | > based on known results. `interactTop` seems to simply constraints on > | > their own, `interactInert` seems to simplify based on being given two > | > similar contraints. > | > > | > By big questions is what exactly `matchFam` does. The argument seems > | > to be the arguments to the type family, but the tuple in the result is > | > less clear. The axiom rule is the proof witness, the second argument I > | > guess is the type arguments you actually care about? What is this used > | for? > | > The last one should be the result type. > | > > | > Attached to that, what are the garantuees about the list of types that > | > you get? I assumed at first they were all flattened, but my other type > | > family is not. I am talking about this piece of code here: > | > > | > ``` > | > matchFamRnil :: [Type] -> Maybe (CoAxiomRule, [Type], Type) > | > matchFamRnil [] = Just (axRnilDef, [], mkRowTy k v []) > | > where binders = mkTemplateKindTyConBinders [liftedTypeKind, > | > liftedTypeKind] > | > [k, v] = map (mkTyVarTy . binderVar) binders matchFamRnil _ > | > = Nothing > | > > | > > | > matchFamRowExt :: [Type] -> Maybe (CoAxiomRule, [Type], Type) > | > matchFamRowExt [_k, _v, x, y, row@(RowTy (MkRowTy k v flds))] = Just > | > (axRowExtDef, [x, y, row], RowTy (MkRowTy k v $ (x, y):flds)) > | > matchFamRowExt [k, v, x, y, _rnil] = Just (axRowExtRNilDef, [k, v], > | > RowTy (MkRowTy k v [(x, y)])) matchFamRowExt _ = Nothing > | > > | > ``` > | > > | > I needed an extra `_rnil` case in `matchFamRowExt` because `RowExt > | > "foo" Int RNil` did not match the first pattern match (the dumped list > | > I got was `[Symbol, Type, "foo", Int, RNil]`). Also, is there a better > | > way to conjure up polykinded variables out of the blue or is this > | > fine? I thought about leaving off that info from the type, but then I > | > would have the same question when trying to implement `typeKind` or > | > `tcTypeKind` (for a non-empty row I can use the kinds of the head of > | > the list, for an empty one I would need polykinded variables) > | > > | > My last question is about CoAxiomRules. The note says that they > | > represent "forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2", but it is not > | > clear for me in what relation the constraints on the left are with the > | > right. From the typeNats it looks like `t1` is the type family applied > | > to the `_1` arguments and `t2` is the calculated result using the `_2` > | > arguments. Why are we not getting just a list of types as inputs? Is > | > the `_1` always a unification/type variable and not really a type you > | > can use to calculate stuff? Also, if I extrapolate my observations to > | > type families without arguments, I would assume that I do not have > | > constraints on the left hand side as `t1` would be the family appied > | > to the arguments (none) and `t2` would be the calculated result from > | > the `_2` args (I do not need anything to return an empty row). Is this > | > correct or am I horribly wrong? > | > > | > > | > Thanks for your time listening to my questions, maybe I can open a PR > | > with a bit of documentation with eventual answers. > | > > | > Cheers, > | > Jan > | > > | > _______________________________________________ > | > ghc-devs mailing list > | > [email protected] > | > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail. > | > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01 > | > %7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d72b4c786c%7C72f988 > | > bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&sdata=VtrN > | > FMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&reserved=0 > | _______________________________________________ > | ghc-devs mailing list > | [email protected] > | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask > | ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- > | devs&data=02%7C01%7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d7 > | 2b4c786c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&a > | mp;sdata=VtrNFMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&reserved=0 _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
