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
