A few questions about BuiltInSynFamily/CoAxiomRules
Jan van Brügge
jan at vanbruegge.de
Wed Aug 28 10:37:24 UTC 2019
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 <ghc-devs-bounces at haskell.org> On Behalf Of Iavor Diatchki
> | Sent: 28 August 2019 01:12
> | To: Jan van Brügge <jan at vanbruegge.de>
> | Cc: ghc-devs at 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 <jan at vanbruegge.de> 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 at 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 at 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
More information about the ghc-devs
mailing list