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

Ok, I managed to answer those two myself. The type families try to match first unflattened and if that fails recursively flatten. My problem was that I messed up the definition of RNil to only match if it gets no arguments. But it does, it gets the inferred kinds! So after fixing that pattern match everything was working. This also makes the first question irrelevant as I get everything needed. Thanks for your help, especially Iavor! Cheers, Jan Am 28.08.19 um 12:37 schrieb Jan van Brügge:

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