A few questions about BuiltInSynFamily/CoAxiomRules

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

A few questions about BuiltInSynFamily/CoAxiomRules

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: A few questions about BuiltInSynFamily/CoAxiomRules

GHC - devs mailing list
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 <[hidden email]> On Behalf Of Iavor Diatchki
|  Sent: 28 August 2019 01:12
|  To: Jan van Brügge <[hidden email]>
|  Cc: [hidden email]
|  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 <[hidden email]> 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
|  > [hidden email]
|  > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.
|  > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&amp;data=02%7C01
|  > %7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d72b4c786c%7C72f988
|  > bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&amp;sdata=VtrN
|  > FMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
|  _______________________________________________
|  ghc-devs mailing list
|  [hidden email]
|  https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
|  ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
|  devs&amp;data=02%7C01%7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d7
|  2b4c786c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&a
|  mp;sdata=VtrNFMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A few questions about BuiltInSynFamily/CoAxiomRules

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 <[hidden email]> On Behalf Of Iavor Diatchki
> |  Sent: 28 August 2019 01:12
> |  To: Jan van Brügge <[hidden email]>
> |  Cc: [hidden email]
> |  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 <[hidden email]> 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
> |  > [hidden email]
> |  > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.
> |  > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&amp;data=02%7C01
> |  > %7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d72b4c786c%7C72f988
> |  > bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&amp;sdata=VtrN
> |  > FMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
> |  _______________________________________________
> |  ghc-devs mailing list
> |  [hidden email]
> |  https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
> |  ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
> |  devs&amp;data=02%7C01%7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d7
> |  2b4c786c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&a
> |  mp;sdata=VtrNFMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A few questions about BuiltInSynFamily/CoAxiomRules

Jan van Brügge
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 <[hidden email]> On Behalf Of Iavor Diatchki
>> |  Sent: 28 August 2019 01:12
>> |  To: Jan van Brügge <[hidden email]>
>> |  Cc: [hidden email]
>> |  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 <[hidden email]> 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
>> |  > [hidden email]
>> |  > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.
>> |  > haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&amp;data=02%7C01
>> |  > %7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d72b4c786c%7C72f988
>> |  > bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&amp;sdata=VtrN
>> |  > FMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
>> |  _______________________________________________
>> |  ghc-devs mailing list
>> |  [hidden email]
>> |  https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
>> |  ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
>> |  devs&amp;data=02%7C01%7Csimonpj%40microsoft.com%7C5dd2f56bf336459df67608d7
>> |  2b4c786c%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637025479769572505&a
>> |  mp;sdata=VtrNFMSiRxfGvDIKDjHYc0Jk9NgUgaRuP07OvZ5qpr8%3D&amp;reserved=0
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs