Re: A few questions about BuiltInSynFamily/CoAxiomRules

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 On Behalf Of Iavor Diatchki | Sent: 28 August 2019 01:12 | To: Jan van Brügge | Cc: ghc-devs@haskell.org | 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 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 | > ghc-devs@haskell.org | > 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 | ghc-devs@haskell.org | 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