Equality constraints (~): type-theory behind them

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

Equality constraints (~): type-theory behind them

AntC
The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies` language extension.

GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a series of papers 2005 to 2008, and IIRC the development wasn't finished in full in GHC until after that. (Superclass constraints took up to about 2010.)

Suppose I wanted just the (~) parts of those implementations. Which would be the best place to look? (The Users Guide doesn't give a reference.) ICFP 2008 'Type Checking with Open Type Functions' shows uses of (~) in user-written code, but doesn't explain it or motivate it as a separate feature.

My specific question is: long before (~), it was possible to write a TypeCast class, with bidirectional FunDeps to improve each type parameter from the other. But for the compiler to see the type improvement at term level, typically you also need a typeCast method and to explicitly wrap a term in it. If you just wrote a term of type `a` in a place where `b` was wanted, the compiler would either fail to see your `TypeCast a b`, or unify the two too eagerly, then infer an overall type that wasn't general enough.

(For that reason, the instance for TypeCast goes through some devious/indirect other classes/instances or exploits separate compilation, to hide what's going on from the compiler's enthusiasm.)

But (~) does some sort of magic: it's a kinda typeclass but without a method. How does it mesh with type improvement in the goldilocks zone: neither too eager nor too lazy?


AntC

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

Adam Gundry-2
Hi AntC [with apologies for the duplicate email],

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X): Modular type inference with local assumptions. JFP 2011.
<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf>.

On the underlying core language, there are various papers starting with
Sulzmann et al. System F with type equality coercions. TLDI 2007.
<https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf>

About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

    foo :: forall a b . a ~ b => [a] -> [b]
    foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:

> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
>
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
>
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
>
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
>
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
>
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
>
>
> AntC


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

AntC
In reply to this post by AntC
On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X):

Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ...

I'm not sure I grok your response on my specific q; to adapt your example slightly, without a signature

    foo2 x@(_: _) = x

GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a signature with bare `b` as the return type, using the (~) to improve it:

    foo2 :: [a] ~ b => [a] -> b

... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?

I'm chiefly concerned about improving bare tyvars under a FunDep. So to take the time-worn example, I want instances morally equivalent to

    data TTrue = TTrue;  data TFalse = TFalse

    class TEq a b r  | a b -> r  where tEq :: a -> b -> r

    instance TEq a a TTrue   where tEq _ _ = TTrue
    instance TEq a b TFalse  where tEq _ _ = TFalse

The FunDeps via CHRs 2006 paper tells me that first instance is supposed to be as if

    instance (r ~ TTrue) => TEq a a r  where ...

but it isn't

    tEq 'a' 'a' :: TFalse      -- returns TFalse, using the first pair of instances
    tEq 'a' 'a' :: TFalse      -- rejected, using the (~) instance: 'Couldn't match type TFalse with TTrue ...'

The 'happily' returning the 'wrong' answer in the first case has caused consternation amongst beginners, and a few Trac tickets.

So what magic is happening with (~) that it can eagerly improve `foo2` but semi-lazily hold back for `tEq`?

Of course I lied about the first-given two instances for TEq: instances are not consistent with Functional Dependency. So I need to resort to overlaps and a (~) and exploit GHC's bogus consistency check:

    instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...

> ... like automatically inferring where `typeCast` needs to be placed

Yes the non-automatic `TypeCast` version

    instance (TypeCast TTrue r) => TEq a a r  where
      tEq _ _ = TTrue         -- rejected 'Couldn't match expected type 'r' with actual type 'TTrue' ...'

      tEq _ _ = typeCast TTrue    -- accepted

Even though `typeCast` is really `id` (after it's jumped through the devious indirection hoops I talked about).

So what I'm trying to understand is not just "where" to place `typeCast` but also "when" in inference it unmasks the unification.


AntC


About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

    foo :: forall a b . a ~ b => [a] -> [b]
    foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
>
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
>
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
>
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
>
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
>
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
>
>
> AntC



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

Tom Schrijvers-2
Hi Anthony,

Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:

Cheers,

Tom

On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden <[hidden email]> wrote:
On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X):

Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ...

I'm not sure I grok your response on my specific q; to adapt your example slightly, without a signature

    foo2 x@(_: _) = x

GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a signature with bare `b` as the return type, using the (~) to improve it:

    foo2 :: [a] ~ b => [a] -> b

... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?

I'm chiefly concerned about improving bare tyvars under a FunDep. So to take the time-worn example, I want instances morally equivalent to

    data TTrue = TTrue;  data TFalse = TFalse

    class TEq a b r  | a b -> r  where tEq :: a -> b -> r

    instance TEq a a TTrue   where tEq _ _ = TTrue
    instance TEq a b TFalse  where tEq _ _ = TFalse

The FunDeps via CHRs 2006 paper tells me that first instance is supposed to be as if

    instance (r ~ TTrue) => TEq a a r  where ...

but it isn't

    tEq 'a' 'a' :: TFalse      -- returns TFalse, using the first pair of instances
    tEq 'a' 'a' :: TFalse      -- rejected, using the (~) instance: 'Couldn't match type TFalse with TTrue ...'

The 'happily' returning the 'wrong' answer in the first case has caused consternation amongst beginners, and a few Trac tickets.

So what magic is happening with (~) that it can eagerly improve `foo2` but semi-lazily hold back for `tEq`?

Of course I lied about the first-given two instances for TEq: instances are not consistent with Functional Dependency. So I need to resort to overlaps and a (~) and exploit GHC's bogus consistency check:

    instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...

> ... like automatically inferring where `typeCast` needs to be placed

Yes the non-automatic `TypeCast` version

    instance (TypeCast TTrue r) => TEq a a r  where
      tEq _ _ = TTrue         -- rejected 'Couldn't match expected type 'r' with actual type 'TTrue' ...'

      tEq _ _ = typeCast TTrue    -- accepted

Even though `typeCast` is really `id` (after it's jumped through the devious indirection hoops I talked about).

So what I'm trying to understand is not just "where" to place `typeCast` but also "when" in inference it unmasks the unification.


AntC


About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

    foo :: forall a b . a ~ b => [a] -> [b]
    foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
>
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
>
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
>
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
>
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
>
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
>
>
> AntC


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


--
prof. dr. ir. Tom Schrijvers

Research Professor
KU Leuven
Department of Computer Science

Celestijnenlaan 200A
3001 Leuven
Belgium
Phone: +32 16 327 830

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

AntC
On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:


Thank you Tom, looks interesting and very applicable. It'll be a few days before I can take a proper look.

I see you compare GHC vs Hugs: good, they differ significantly in the details of implementation. I found Hugs well-principled, whereas GHC is far too sloppy in what instances it accepts (but then you find they're unusable).

Maybe I scanned your paper too quickly, but it looks like you insist on non-overlapping instances (or that if instances overlap, they are 'confluent', in the terminology of the 2005~2008 work; or 'coincident' in Richard E's work). And the 2006 CHRs paper takes the same decision. That's a big disappointment: I think the combo of Overlap+FunDeps makes sense (you need to use (~) constraints -- hence this thread), and there's plenty of code using the combo -- including the HList 2004 paper (with `TypeCast`).

You can make that combo work with GHC, as did HList. But it's hazardous because of GHC's sloppiness/bogusness. You can't make that combo work with Hugs as released; but because it's a better principled platform, a limited-scope tweak to the compiler makes it work beautifully. Documented here: https://ghc.haskell.org/trac/ghc/ticket/15632#comment:2


AntC



On Sat, Dec 8, 2018 at 6:42 AM Anthony Clayden <[hidden email]> wrote:
On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:

Regarding inference, the place that comes to mind is Vytiniotis et al.
OutsideIn(X):

Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ...

I'm not sure I grok your response on my specific q; to adapt your example slightly, without a signature

    foo2 x@(_: _) = x

GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a signature with bare `b` as the return type, using the (~) to improve it:

    foo2 :: [a] ~ b => [a] -> b

... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect?

I'm chiefly concerned about improving bare tyvars under a FunDep. So to take the time-worn example, I want instances morally equivalent to

    data TTrue = TTrue;  data TFalse = TFalse

    class TEq a b r  | a b -> r  where tEq :: a -> b -> r

    instance TEq a a TTrue   where tEq _ _ = TTrue
    instance TEq a b TFalse  where tEq _ _ = TFalse

The FunDeps via CHRs 2006 paper tells me that first instance is supposed to be as if

    instance (r ~ TTrue) => TEq a a r  where ...

but it isn't

    tEq 'a' 'a' :: TFalse      -- returns TFalse, using the first pair of instances
    tEq 'a' 'a' :: TFalse      -- rejected, using the (~) instance: 'Couldn't match type TFalse with TTrue ...'

The 'happily' returning the 'wrong' answer in the first case has caused consternation amongst beginners, and a few Trac tickets.

So what magic is happening with (~) that it can eagerly improve `foo2` but semi-lazily hold back for `tEq`?

Of course I lied about the first-given two instances for TEq: instances are not consistent with Functional Dependency. So I need to resort to overlaps and a (~) and exploit GHC's bogus consistency check:

    instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r  where ...

> ... like automatically inferring where `typeCast` needs to be placed

Yes the non-automatic `TypeCast` version

    instance (TypeCast TTrue r) => TEq a a r  where
      tEq _ _ = TTrue         -- rejected 'Couldn't match expected type 'r' with actual type 'TTrue' ...'

      tEq _ _ = typeCast TTrue    -- accepted

Even though `typeCast` is really `id` (after it's jumped through the devious indirection hoops I talked about).

So what I'm trying to understand is not just "where" to place `typeCast` but also "when" in inference it unmasks the unification.


AntC


About your specific question, if a wanted constraint `a ~ b` can be
solved by unifying `a` with `b`, then GHC is free to do so (in a sense,
either parameter of (~) can be improved from the other). The real
difference with `TypeCast` arises when local equality assumptions (given
constraints) are involved, because then there may be wanted constraints
that cannot be solved by unification but can be solved by exploiting the
local assumptions.

For example, consider this function:

    foo :: forall a b . a ~ b => [a] -> [b]
    foo x = x

When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises
(because `x` has type `[a]` and is used in a place where `[b]` is
expected). Since `a` and `b` are universally quantified variables, this
cannot be solved by unification. However, the local assumption (given
constraint) `a ~ b` can be used to solve this wanted.

This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).

Hope this helps,

Adam


On 06/12/2018 12:01, Anthony Clayden wrote:
> The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies`
> language extension.
>
> GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a
> series of papers 2005 to 2008, and IIRC the development wasn't finished
> in full in GHC until after that. (Superclass constraints took up to
> about 2010.)
>
> Suppose I wanted just the (~) parts of those implementations. Which
> would be the best place to look? (The Users Guide doesn't give a
> reference.) ICFP 2008 'Type Checking with Open Type Functions' shows
> uses of (~) in user-written code, but doesn't explain it or motivate it
> as a separate feature.
>
> My specific question is: long before (~), it was possible to write a
> TypeCast class, with bidirectional FunDeps to improve each type
> parameter from the other. But for the compiler to see the type
> improvement at term level, typically you also need a typeCast method and
> to explicitly wrap a term in it. If you just wrote a term of type `a` in
> a place where `b` was wanted, the compiler would either fail to see your
> `TypeCast a b`, or unify the two too eagerly, then infer an overall type
> that wasn't general enough.
>
> (For that reason, the instance for TypeCast goes through some
> devious/indirect other classes/instances or exploits separate
> compilation, to hide what's going on from the compiler's enthusiasm.)
>
> But (~) does some sort of magic: it's a kinda typeclass but without a
> method. How does it mesh with type improvement in the goldilocks zone:
> neither too eager nor too lazy?
>
>
> AntC


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users



--
prof. dr. ir. Tom Schrijvers

Research Professor
KU Leuven
Department of Computer Science

Phone: +32 16 327 830

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

AntC

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <[hidden email]> wrote:
On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:


Thank you Tom, looks interesting and very applicable. It'll be a few days before I can take a proper look.

So the paper's main motivation is wrt Trac #9670. I've added some comments there, including a link to your paper. In particular, both GHC and Hugs will infer the 'right' type -- i.e. as improved from the FunDep. But neither allows you to use that improvement to write the desired function `f`. It's a phasing of inference thing(?)

I feel I'm not getting much light shed. No amount of adding `(~)` in GHC nor `TypeCast`+`typeCast` method in Hugs will get #9670 function `f` to compile. So my 'specific example' earlier in this thread shows `(~)` is moderately eager/more eager than FunDeps alone, but not eager enough for #9670.

IOW from Adam's comment about "inferring where `typeCast` needs to be placed", it seems there's no such place. Perhaps because class `C` has no methods(?)

Yes, as per your+Georgios' paper, replacing the FunDep with an Assoc Type and superclass `(~)` constraint is eager enough. That's not telling me why the FunDep+`(~)` constraint on the instances or function signatures isn't so eager.

From the #9670 comment by spj: it's historically to do with an inability to represent evidence under System FC. It seems GHC is taking absence of evidence as evidence of absence, even though it's able to infer the 'right' type. 

AntC

On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote:
...
This is rather like automatically inferring where `typeCast` needs to be
placed (indeed, at the Core level there is a construct for casting by an
equality proof, which plays much the same role).


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

Oliver Charles-3
On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden
<[hidden email]> wrote:

> So the paper's main motivation is wrt Trac #9670.

Are you sure you mean #9670?
https://ghc.haskell.org/trac/ghc/ticket/9670 is "Make Data.List.tails
a good producer for list fusion" and has nothing to do with functional
dependencies.
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

AntC
On Sat, 22 Dec 2018 at 8:01 PM, Oliver Charles wrote:

On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden
<[hidden email]> wrote:

> So the paper's main motivation is wrt Trac #9670.

Are you sure you mean #9670?
Oops. Thanks for the catch Oliver. That should be #9627. (One of the tickets to do with FunDeps and type improvement ends in 70 ;-)

AntC

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

AntC
In reply to this post by AntC


On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <[hidden email]> wrote:

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <[hidden email]> wrote:
On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:



I feel I'm not getting much light shed. No amount of adding `(~)` in GHC nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to compile. So my 'specific example' earlier in this thread shows `(~)` is moderately eager/more eager than FunDeps alone, but not eager enough for #9627.


Can anybody explain @yav's comment here 
https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613 "currently equality constraints have no run-time evidence associated with them".

Haskell has type-erasure semantics. Why would I need any _run-time_ evidence for anything to do with type improvement? What impact would the lack of evidence have at run-time?

Does this mean `(~)` constraints don't produce evidence at compile time? Which is also the difficulty for type improvement under FunDeps.

(I tried a type family to achieve the same effect as `(~)` with an injective TF. No improvement in improvement.)


AntC



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints (~): type-theory behind them

Brandon Allbery
I think the point is more that runtime evidence means passing an additional type witness around, potentially changing generated code and even behavior (if this causes dictionary passing where none had been needed previously). It's not addressing your question.

On Sat, Dec 22, 2018 at 11:48 PM Anthony Clayden <[hidden email]> wrote:


On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden <[hidden email]> wrote:

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden <[hidden email]> wrote:
On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote:
Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem:



I feel I'm not getting much light shed. No amount of adding `(~)` in GHC nor `TypeCast`+`typeCast` method in Hugs will get #9627 function `f` to compile. So my 'specific example' earlier in this thread shows `(~)` is moderately eager/more eager than FunDeps alone, but not eager enough for #9627.


Can anybody explain @yav's comment here 
https://github.com/ghc-proposals/ghc-proposals/pull/158#issuecomment-449590613 "currently equality constraints have no run-time evidence associated with them".

Haskell has type-erasure semantics. Why would I need any _run-time_ evidence for anything to do with type improvement? What impact would the lack of evidence have at run-time?

Does this mean `(~)` constraints don't produce evidence at compile time? Which is also the difficulty for type improvement under FunDeps.

(I tried a type family to achieve the same effect as `(~)` with an injective TF. No improvement in improvement.)


AntC


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users


--
brandon s allbery kf8nh

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users