[GHC] #14917: Allow levity polymorhism in binding position

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

[GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
           Reporter:  andrewthad     |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  LevityPolymorphism                 |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The main problem with levity polymorphism in a binding position is that
 it's impossible to do codegen since the calling convention depending on
 the instantiation of the runtime representation variable. From the paper,
 we have the following rejected example code:

 {{{
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
 }}}

 However, if you are able to inline the function, this problem disappears.
 You would need a guarantee stronger than what the `INLINE` pragma provides
 though since the `INLINE` pragma still allows the function to be fed as an
 argument to a higher-order function. I'll refer to a hypothetical new
 pragma as `INLINE MANDATE`. This pragma causes a compile-time error to be
 admitted if the function is ever used in a way that would cause it to not
 be inlined. Now `bTwice` would be writeable:

 {{{
 {-# INLINE MANDATE #-}
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
 }}}

 The function definition would be provide in the `.hi` file just as it
 would be for a function marked as `INLINE`, but unlike the `INLINE`
 counterpart, there would be no generated code for this function, since
 generating the code would be impossible.

 I have several uses for this in mind. I often want a levity-polymorphic
 variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation,
 but I could write:

 {{{
 -- This newtype is already allowed today
 newtype STL s (a :: TYPE r) = STL (State# s -> (# s, a #) #)

 intA, intB, intC :: STL s Int#
 wordA, wordB :: Int# -> STL s Word#

 {-# INLINE MANDATE #-}
 (>>=.) :: STL s a -> (a -> STL s b) -> STL s b
 STL a >>=. g = STL (\s0 -> case a s0 of
     (# s1, v #) -> case g v of
       STL f -> f s1

 myFunc :: STL s Word#
 myFunc =
   intA >>=. \a ->
   intB >>=. \b ->
   intC >>=. \c ->
   wordA a >>=. \wa ->
   wordB b >>=. \wb ->
   ... -- do something with the data
 }}}

 I would appreciate any feedback on this. If there's something that makes
 this fundamentally impossible, that would be good to know. Or if other
 people feel like this would be useful, that would be good to know as well.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I'm very cautious about this.

 Sometimes you can't inline.  For example a recursive function.  And
 {{{
 f :: Int -> Int
 {-# INLINE f #-}
 f x = blah

 g xs = map f xs
 }}}
 I can't inline `f` here; or if I do I'll get a `\x`.

 In our paper we prove that, in our system, you never get a situation where
 you don't know the runtime reprsentation of a value you have to
 manipulate.  I don't see how to produce a similar proof with weaker
 restrictions.

 Runtime code cloining, like .NET, is a good path.  But it comes at a
 price!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by andrewthad):

 I agree that it isn’t always possible to inline. Higher order functions,
 like map, don’t allow it. Maybe the most accurate way to describe what I
 want is for there to be a way to make fully saturated calls to functions
 with levity polymorphic binders. It seems like it should be possible to
 perform a check for unsaturated calls. Recursive levity polymorphic
 functions would not be allowed, but there’s still a lot of useful stuff
 that could be done.

 Your point about the proof that the paper offers is good. My suggested
 addition would mess up that proof, which would be bad. What if (and this
 is total speculation since I don’t understand type theory) you had two
 universes that functions could live in. One universe is this one that we
 currently have. There are no levity polymorphic binders, and in this
 universe, you have the guarantee that you always know the runtime
 representation of values that need to be manipulated. In the second
 universe, levity polymorphism would be unrestricted. Technically, this
 universe would be a superset of the first one. But it may be helpful to
 think of them as separate universes since in GHC, codegen could only
 happen for functions in the first universe. Functions from 1 could be
 freely used in 2. Functions from 2 could be freely used in 2 as well. But,
 functions from 2 could not be freely used in 1. They would need to be
 specialized to satisfy the restrictions around levity polymorphism. In
 practice, this specialization would take the form of inlining.

 So, I guess that would mean that the function arrow would have a weird
 kind, since it could create types belonging to universe 1 or 2. And I have
 no idea how function application would typecheck.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I actually think this is a good idea.

 Simon's right in that figuring out exactly when you can inline can be
 tricky. But this logic is already in the compiler (in the inliner!) and so
 we can perhaps work it into the desugarer (which is where levity-
 polymorphism errors are issued). It's possible we'll have a hard time
 producing sensible error messages, but I think we'll be able to surmount
 that challenge.

 As to the proof: I'm not concerned. The proof is about Core. The proposed
 change wouldn't affect Core at all. Core still wouldn't have levity-
 polymorphic binders. (Unfoldings might, but not actual Core programs that
 will be compiled.) We can think of this proposal as suggesting "function
 templates", where these templates are stand-ins for a (perhaps infinite)
 family of levity-monomorphic functions.

 The implementation of this would be fiddly, but I don't see any true
 obstacles to it. And it does seem very silly that users can't reuse their
 typing for a function as simple as `twice`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 If something changes in the inliner could working levity-poly definitions
 fail?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by andrewthad):

 @Iceland_jack  I believe that the inlining phase (or phases) happens after
 type checking, so this couldn’t even be done during the usual inlining
 phase.  You would need something similar to the inlining phase that
 happens prior to type checking.  The only  things allowed to inline during
 this phase would be  fully saturated calls to functions with levity
 polymorphic binders ( maybe function template, as Richard suggests, is an
 appropriate name for it).  This is why Richard says that it would be hard
 to produce sensible error messages. So, I don’t think that changes to the
 inliner  could mess this up because this would be a separate and unusual
 inlining phase.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I am a bit less optimistic than Richard (in comment:3).  You imply that
 all the inlining could be done in the desugarer; but that can only work if
 you could see all calls.

 GHC does already have the notion of a "compulsory unfolding" (see
 `CoreSyn.UnfoldingSource`).  Bindings with a compulsory unfolding ''do not
 have a binding at all'', so they must be inlined at every call site.  That
 fits with the proposal here because we can't implement the levity-
 polymorphic code, so we can't compile code for it.

 We'd still somehow need to check that, after the inlining, the levity-
 polymorphism had vanished, and give a decent error message if not.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Yes, I was thinking of compulsory unfoldings without realizing it.

 I think the existing check for levity-polymorphic arguments in the
 desugarer (which wouldn't change under this proposal) would catch cases
 where a levity-polymorphic function wasn't sufficiently specialized. All
 that would be left to check for is that the compulsory unfolding would
 actually work (and that the function was sufficiently saturated). If it
 doesn't, I think we would be able to report a sensible error, because we
 at least have the name of the thing that didn't unfold.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 You know, this is all very much like unboxed tuples. Unboxed tuples are
 themselves levity polymorphic, must be levity monomorphic at use sites,
 and have a compulsory unfolding. So perhaps much of the plumbing is
 installed already.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > You know, this is all very much like unboxed tuples.

 But do we allow `(#,,#) x y` or stuff like that with a possibly-
 unsaturated use of the data constructor?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Sure we do. I have not explored ''how'' we do, but sure we do. This
 program compiles and runs:

 {{{#!hs
 data List (b :: TYPE (TupleRep [IntRep, DoubleRep, LiftedRep])) = Nil |
 Cons b (List b)

 mapUbx :: forall (a :: Type) (b :: TYPE (TupleRep [IntRep, DoubleRep,
 LiftedRep])). (a -> b) -> [a] -> List b
 mapUbx _ [] = Nil
 mapUbx f (x : xs) = Cons (f x) (mapUbx f xs)

 blargh :: forall a. Int# -> Double# -> a -> (# Int#, Double#, a #)
 blargh x y = (#,,#) x y

 strange = mapUbx (blargh 3# 2.78##) [True, False]

 printList :: Show b => List (# Int#, Double#, b #) -> IO ()
 printList Nil = return ()
 printList (Cons (# n, d, b #) xs) = do
   print (I# n)
   print (D# d)
   print b
   printList xs

 main = do
   printList strange
 }}}

 We probably just eta-expand `blargh`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Could we skirt the problem using typeclass machinery? Instead of

 {{{#!hs
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a
 }}}

 What if we have

 {{{#!hs
 bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). KnownRep r => Bool → a → (a →
 a) → a
 }}}

 To call this function, we consult the `KnownRep` dictionary to discover
 its calling conventions. Obviously everything will be terrible if it
 doesn't specialize, but maybe there's a way to make it work soundly
 otherwise?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorhism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorhism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by dfeuer):

 * cc: dfeuer (added)


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorphism in binding position (was: Allow levity polymorhism in binding position)

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorphism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by andrewthad):

 There was a reddit discussion[1] that reminded me of this, and it got a
 tangential but related idea going in my mind. I wonder if there's any
 connection between user-defined functions with a compulsory unfolding and
 `UNPACK` on polymorphic fields in a data constructor (currently disallowed
 because they result in code that cannot be compiled). Roughly, the idea
 was that a compulsory unfolding would be required for functions that
 target data types with unpacked polymorphic fields. For example:

 {{{
 data Foo a = Foo {-# UNPACK -#} !Int {-# UNPACK #-} !a

 {-# INLINE MANDATE useFoo #-}
 useFoo :: Foo a -> a
 useFoo (Foo _ a) = a
 }}}

 This would also lift the restriction on levity-polymorphic fields in a
 data constructor. There are a bunch of other problems with this that may
 not be possible to resolve. How does pattern matching actually work with
 this? How can `Foo Word` be stored inside of another data type? Anyway,
 I'm not convinced this could actually go anywhere, but I thought I'd jot
 it down.

 [1]
 https://www.reddit.com/r/haskell/comments/8a5w1n/new_package_unpackedcontainers/

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorphism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by josef):

 I've thought about this problem for some time, but never written down
 my ideas before. Now seemed like a good time to speak up though :-) Below
 are some hopefully coherenet notes.

 I'd introduce a new quantifier (let's call it "V") which provides
 '''template polymorphism'''.  This quantifier can quantify over all kinds,
 even levity polymorphic things.  The idea is that whenever a function
 of template polymorphic type is called, a new copy of the function
 will be created, specialized with the instantiated type for its
 template polymorphic type variables.

 Example:

 {{{
 id :: V r (a :: TYPE r). a -> a
 id a = a
 }}}

 When we use it like in an expression like this `id #5` or `id "foo"`
 the typechecker creates new bindings `id_#_Int#` and `id_*_String`. These
 new bindings are then used as part of elaborating the expressions:
 `id_#_Int# #5` and `id_*_String "foo"`.

 {{{
 id_#_Int# :: Int# -> Int#
 id_#_Int# a = a

 id_*_String :: String -> String
 id_*_String a = a
 }}}

 More formally: A call to a template polymorphic function must
 instantiate all template polymorphic type parameters. These parameters
 must be instantiated with either fully ground types without any
 variables, or variables bound by "V", the template polymorphic
 quantifier.

 A trivial point, that I still want to point out: given two (or more)
 calls to the same template polymorphic function with the same type
 instantiation only generates one new specialization.

 Most likely a more sophisticated naming scheme than the one I've used
 here will be needed to ensure that the names of the new bindings are
 unique.

 The quantifier is only allowed to be used on the top-level and must
 appear before any usual quantifiers. I.e. template polymorphism is rank-1.

 Quantified template polymorphism, i.e. having class constraints on
 template polymorphic type variables is not a problem.

 == Recursion ==

 It is perfectly possible to support monomorphic recursion for template
 polymorphism. In fact, the elaboration outlined above supports
 monomorphic recursion out of the box. The recursive call inside of
 template polymorphic function would generate the same specialization
 as a call from outside the function, and since we don't generate
 multiple specializations, the call will simply be specialized to a
 recursive call in the new specialized function.


 It is likely possible to support special cases of polymorphic
 recursion, but it is not clear to me that it is worth the extra work.

 == Modules ==

 When exporting a template polymorphic function, it's specializations
 should also be exported, to avoid re-generating them. However, the
 importing module will have to creating its own new specializations if
 needed.

 This can lead to a situation where a module has two imports which
 exports the same specialization of a function they in turn
 imported. But there is no real problem here, because it doesn't matter
 which one we pick since both specializations will be the same.

 == Extensions ==

 One of the interesting things about this proposal is that generalizes
 nicely
 to data types.

 Example:

 {{{
 data List (V r) (a :: TYPE r) = Cons a (List r a) | Nil
 }}}

 This way we get a list data type which can be used at any kind. After
 type checking and elaboration we will have one list data type for
 each runtime representation.

 However, supporting specialization in different modules might require a
 bit of thought.

 == Final thoughts ==

 The gist of this proposal is that it gives control over optimization
 to the library writer, similarly to the RULES pragma. Though it will not
 help any existing programs go faster.

 I'd really like to see something like this in GHC. Unfortunately, I don't
 have the cycles to flesh out this proposal and implement it. But I'd be
 happy to advice if someone wants to have a go at it.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:15>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorphism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I, too, have pondered template polymorphism for some time, but never
 fleshed it out even to this level. There are a few problems with this
 design, however:

 >  More formally: A call to a template polymorphic function must
 instantiate all template polymorphic type parameters. These parameters
 must be instantiated with either fully ground types without any variables,
 or variables bound by "V", the template polymorphic quantifier.

 This means that, with your `id` definition, you couldn't have

 {{{#!hs
 idList :: [a] -> [a]
 idList = id
 }}}

 even though you could have

 {{{#!hs
 idListInt :: [Int] -> [Int]
 idListInt = id
 }}}

 So it seems template polymorphism would be infectious, generally requiring
 callers of template-polymorphic functions also to be template-polymorphic.
 I don't think that's a good thing.

 On the flip side, I don't see concretely why we need the "no variables"
 restriction.

 > It is likely possible to support special cases of polymorphic recursion,
 but it is not clear to me that it is worth the extra work.

 Generally, these schemes fail on polymorphic recursion, and I think we
 should do so here, too.

 > This can lead to a situation where a module has two imports which
 exports the same specialization of a function they in turn imported. But
 there is no real problem here, because it doesn't matter which one we pick
 since both specializations will be the same.

 I think there ''is'' a real problem here. First off, it means that the
 `.o` files that GHC produces won't be able to be linked by, e.g., `ld`:
 multiple `.o` files might have the same definitions. In the end, I think
 we'd have to implement some deduplication algorithm during linking, or end
 up with horrid code bloat.

 > One of the interesting things about this proposal is that generalizes
 nicely to data types.

 Under your "no variables" rule, this `List` type would have to be
 specialized at every possible data parameter. I'm worried about bloat.

 > However, supporting [data] specialization in different modules might
 require a bit of thought.

 This is also a thorny question. Here, we absolutely have to get
 deduplication correct, as it's a matter of correctness, not just
 efficiency (in size of the executable).

 One unaddressed question here is: what restrictions would there be on
 template-polymorphic levity-polymorphic variables? Presumably, none, but
 I'm not sure.

 Also, how is this different from the "compulsory unfoldings" idea earlier
 in this thread (started in comment:3)? The user declares template
 polymorphism directly (the compulsory unfoldings idea didn't have any user
 direction -- but perhaps it should have), and the specializations here
 happen by creating new bindings instead of inlining, but I'm not sure a
 user would really see the difference here.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:16>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

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

Re: [GHC] #14917: Allow levity polymorphism in binding position

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#14917: Allow levity polymorphism in binding position
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.2
      Resolution:                    |             Keywords:
                                     |  LevityPolymorphism
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by sgraf):

 Another place where this could be useful is for abstracting the pattern in
 [https://hackage.haskell.org/package/base-4.11.0.0/docs/src/GHC.Enum.html#efdtIntUpFB
 efdt{Word,Int}{Up,Dn}FB].

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14917#comment:17>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets