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