Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-16 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  simonpj 
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  7.8.1   
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
Changes (by simonpj):

 * cc: Conor.McBride@…, sweirich@… (added)


Comment:

 Re the sketchiness, is your worry the following?
  * Even though the type `Empty` has no data constructors, there are terms
 with type `Empty`, namely diverging ones, such as `undefined :: Empty`.
  * But are there any '''types''' with '''kind''' `Empty`?  You might think
 "no" since we don't have divergent type terms.  But there is one, namely
 `(Any Empty)`.

 So, is that a problem?  Adding Conor to the cc list.

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-16 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  simonpj 
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  7.8.1   
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--

Comment(by diatchki):

 I updated `GHC.TypeLits` to avoid using `Any` as a constructor, so now we
 should be able to convert it to a type function.

 In a previous e-mail I mentioned some "sketchiness" that occurs when using
 `Any` (in either form) with empty kinds.  Here is an example to illustrate
 the issue:
 {{{
 data {-kind-} Empty

 data T (a :: Empty) = C deriving Show

 main = print C -- what is the type of C here?
 }}}
 The issue is that in `main`: constructor `C` is of type `T Any`, with
 `Any` of kind `Empty`.  However, kind `Empty` has no members, so what does
 `Any` refer to?

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-16 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  simonpj 
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  7.8.1   
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
Changes (by adamgundry):

 * cc: adam.gundry@… (added)


Comment:

 I agree that `Any` should be a type function: to pass kinds as arguments,
 the proxy workaround is the right thing for now, at least until we get
 explicit type/kind application.

 Richard, I think your proposed constraint simplification is sound, but I
 don't really understand the advantage over Simon's version. You are
 introducing fresh (untouchable?) variables `a1` and `a2` instead of `Fst
 a` and `Snd a`, but they don't get you any further. It doesn't matter that
 `Fst` and `Snd` are not injective, because the point of the decomposition
 into `Fst a ~ t1` and `Snd a ~ t2` is not to solve for `a` (which is
 untouchable anyway), but that we might be able to solve for `t1` or `t2`
 if one of them is a variable, or we might have other given constraints on
 the projections.

 In general, adding support for eta to the constraint solver means it
 should never get stuck because an inhabitant of a pair (or other record)
 kind is not canonical. Certainly type family axioms `F '(a, b) = t` should
 be applicable even if the argument is not a canonical pair, but typeclass
 instances exhibit the same behaviour. For example, given the definitions

 {{{
   class Foo (x :: '(a, b))
   instance Foo '(a, b)
 }}}

 we should be able to solve class constraints like `Foo t` using the
 existing instance.

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-15 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  simonpj 
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  7.8.1   
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
Changes (by igloo):

  * owner:  => simonpj
  * milestone:  => 7.8.1


-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-12 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
Changes (by goldfire):

 * cc: eir@… (added)


Comment:

 Adding some discussion that happened on the email thread:

 The axioms that Simon mentioned:

 {{{
 axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
 axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
 axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
 }}}

 The last two axioms are the straightforward compilations of the type
 families {{{Fst}}} and {{{Snd}}} -- nothing new is needed to create these.
 The first is the challenge and will require some type inference magic.

 

 When trying to solve

 {{{
  [W]  (a:'(k1,ks)) ~ '( t1, t2 )
 }}}

 (where {{{a}}} is untouchable), Simon suggested simplifying to

 {{{
  [W]   '(Fst a, Snd a) ~ '( t1, t2)
 }}}

 I don't think that's the right replacement. The next natural step would be
 decomposition, leading to {{{(Fst a ~ t1)}}} and {{{(Snd a ~ t2)}}}, which
 would then get stuck, because {{{Fst}}} and {{{Snd}}} aren't injective.
 So, I would say we need

 {{{
  a1, a2 fresh
  [G] a ~ '(a1, a2)
  [W] '(a1, a2) ~ '(t1, t2)
 }}}

 which would then decompose correctly. As I write this, I'm worried about
 that freshness condition... what if {{{a}}} appears multiple times in the
 type? We would either need to guarantee that {{{a1}}} and {{{a2}}} are the
 same each time, or create new {{{[W]}}} constraints that {{{a1 ~ a1'}}},
 etc. But, maybe this is easier in practice than it seems. Type inference
 experts?

 Simon is a bit concerned about constraints like

 {{{
  F a ~ e
 }}}

 where {{{a:'(k1,k2)}}}, and we have a type instance like {{{F '(a,b) = ...
 }}}.

 It seems to me that the proper eta-expansion (a ~ '(Fst a, Snd a)) would
 work here.

 

 As for {{{Any}}}, (as Nick pointed out and Iavor elaborated) there is a
 workaround that Iavor and I can use involving the promoted version of

 {{{
 data KindProxy (a :: *) = KindProxy
 }}}

 to make kind classes and such. So, I think it's OK to relegate {{{Any}}}
 to a type function. Objections?

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

Re: [GHC] #7259: Eta expansion of products in System FC

2012-10-12 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
Changes (by nfrisby):

 * cc: nfrisby (added)


-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

[GHC] #7259: Eta expansion of products in System FC

2012-09-21 Thread GHC 
#7259: Eta expansion of products in System FC
-+--
Reporter:  simonpj   |   Owner:  
Type:  bug   |  Status:  new 
Priority:  normal|   Milestone:  
   Component:  Compiler  | Version:  7.6.1   
Keywords:|  Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  | Failure:  None/Unknown
  Difficulty:  Unknown   |Testcase:  
   Blockedby:|Blocking:  
 Related:|  
-+--
 This ticket is to capture the ideas in these GHC-users threads:
 [http://www.haskell.org/pipermail/glasgow-haskell-
 users/2012-August/022790.html PolyKinds Aug 2012] and
 [http://www.haskell.org/pipermail/glasgow-haskell-
 users/2012-September/thread.html PolyKinds Sept 2012]

  * We want to add eta-rules to FC.  Sticking to pairs for now, that would
 amount to adding two new type functions (Fst, Snd), and three new, built-
 in axioms
 {{{
 axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
 axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
 axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
 }}}
   Generalising to arbitrary products looks feasible.

  * Adding these axioms would make FC inconsistent, because
 {{{
 axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
 }}}
   and that has two different type constructors on each side.  However, I
 think is readily solved: see below under "Fixing Any"

  * Even in the absence of Any, it's not 100% obvious that adding the above
 eta axioms retains consistency of FC.  I believe that Richard is
 volunteering to check this out.  Right, Richard?

 == Type inference ==

 I'm a little unclear about the implications for inference.  One route
 might be this.   Suppose we are trying to solve a constraint
 {{{
  [W]  (a:'(k1,ks)) ~ '( t1, t2 )
 }}}
 where a is an untouchable type variable.  (if it was touchable we'd simply
 unify it.)  Then we can replace it with a constraint
 {{{
 [W]   '(Fst a, Snd a) ~ '( t1, t2)
 }}}
 Is that it?  Or do we need more?  I'm a bit concerned about constraints
 like
 {{{
 F a ~ e
 }}}
 where `a:'(k1,k2)`, and we have a type instance like  `F '(a,b) = ...`

 Anything else?

 I don't really want to eagerly eta-expand every type variable, because (a)
 we'll bloat the constraints and (b) we might get silly error messages.
 For (b) consider the insoluble constraint
 {{{
 [W]  a~b
 }}}
 where `a` and `b` are both skolems of kind `'(k1,k2)`. If we eta-expand
 both we'll get two insoluble constraints `(Fst a ~ Fst b)` and `(Snd a ~
 Snd b)`, and we DEFINITELY don't want to report that as a type error!

 Someone pointed out that Agda grapples with this problem and we should
 talk to them.


 == Fixing Any ==

  * I think we can fix the Any problem readily by making Any into a type
 family, that has no instances.   We certainly allow equalities with a type
 '''family''' application on the left and a type constructor on the right.

  I have implemented this change already... it seems like a good plan.

  * Several people have asked why we need Any at all.  Consider this source
 program
 {{{
  reverse []
 }}}
   At what type should we instantiate `reverse` and the empty list `[]`?
 Any type will do, but we must choose one; FC doesn't have unbound type
 variables. So I instantiate it at `(Any *)`:
 {{{
  reverse (Any *) ([] (Any *))
 }}}
   Why is Any poly-kinded?  Because the above ambiguity situation sometimes
 arises at other kinds.

  * I'm betting that making Any into a family will mess up Richard's
 (entirely separate) use of `(Any k)` as a proxy for a kind argument `k`;
 because now `(Any k1 ~ Any k2)` does not entail `(k1~k2)`. See also the
 module `GHC.TypeLits` in `base`.

  We can't solve this by making `Any` to be an ''injective'' type family,
 because the use in `TypeLits` uses it in a type-class instance, and you
 can't match on type families!

-- 
Ticket URL: 
GHC 
The Glasgow Haskell Compiler

___
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs