A few questions about BuiltInSynFamily/CoAxiomRules

[Iavor Diatchki]

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
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs