Hi devs,
Apologies if I'm missing context.
Is it more better that "Unlifted" kind is other name, such as
"BoxedUnlifted", "Bul", "%",... ?
I'm studying Unlifted data types [1].
It's good proposals to optimize code by users.
But I worry that newcomers may be confusing about its kind name.
In my
On Wed, Oct 28, 2015 at 9:19 AM, Richard Eisenberg
wrote:
> I don't have terribly much to add, but I do want to counter one point:
>
> On Oct 28, 2015, at 5:48 AM, Edward Kmett wrote:
> > There are situations where we are truly polymorphic in lifting, e.g.
> (==) from Eq and compare from Ord do
On Wed, Oct 28, 2015 at 5:05 AM, Simon Peyton Jones
wrote:
> I'm out of bandwidth at the moment, but let me just remark that this is
> swampy territory. It's easy to mess up.
>
> A particular challenge is polymorphism:
>
> map :: forall a b. (a->b) -> [a] -> [b]
> map f (x:xs) = (f x) : (map
I don't have terribly much to add, but I do want to counter one point:
On Oct 28, 2015, at 5:48 AM, Edward Kmett wrote:
> There are situations where we are truly polymorphic in lifting, e.g. (==)
> from Eq and compare from Ord don't care if the arguments of type 'a' are
> lifted or not.
But
umbrella. That is why trying to tease out the small
handful of cases where we are truly parametric in levity seems interesting.
Finding out some situations existed where we really don't care if a type is
lifted or not was eye opening to me personally, at least.
-Edward
> | -O
-
| From: Dan Doel [mailto:dan.d...@gmail.com]
| Sent: 27 October 2015 23:42
| To: Richard Eisenberg
| Cc: Simon Peyton Jones; ghc-devs
| Subject: Re: Unlifted data types
|
| Hello,
|
| I've added a section with my notes on the minimal semantics required to
| address what Haskell
The idea of treating !S as a subtype of S and then relying on the potential
for new impredicativity machinery to let us just talk about how !S <= S
makes me really happy.
data Nat = Z | S !Nat
Pattern matching on S could give back the tighter type !Nat rather than Nat
for the argument, and if we
Hello,
I've added a section with my notes on the minimal semantics required
to address what Haskell lacks with respect to strict types.
Ed Kmett pointed me to some stuff that I think may fix all the
problems with the !T sort of solution. It builds on the new constraint
being considered for handli
On Oct 8, 2015, at 6:02 AM, Simon Peyton Jones wrote:
> What's the wiki page?
https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
On Thu, Oct 8, 2015 at 6:02 AM, Simon Peyton Jones
wrote:
> | I've added a section on parametric levity polymorphism to the wiki.
> | Sorry it took so long.
>
> What's the wiki page?
>
> Simon
> |
> | I might add some thoughts about first-c
| I've added a section on parametric levity polymorphism to the wiki.
| Sorry it took so long.
What's the wiki page?
Simon
|
| I might add some thoughts about first-class `!a` being the only
| semantic hole in our current strict data type situation later if I
| remember to do so.
___
I've added a section on parametric levity polymorphism to the wiki.
Sorry it took so long.
I might add some thoughts about first-class `!a` being the only
semantic hole in our current strict data type situation later if I
remember to do so.
On Thu, Sep 10, 2015 at 10:26 AM, Richard Eisenberg wro
I'm not so sure how useful an observation this is, but Dunfield
had a paper at this very ICFP "Elaborating Evaluation-Order
Polymorphism". He argues that polymorphism over evaluation
order should be thought of as a form of intersection type.
Edward
Excerpts from Richard Eisenberg's message of 20
On Sep 11, 2015, at 4:28 AM, Roman Cheplyaka wrote:
> On 11/09/15 06:22, Carter Schonwald wrote:
>> Would this allow having a strict monoid instance for maybe, given the
>> right hinting at the use site?
>
> That's a fantastic idea, especially if it could be generalized to
> Applicative functor
On 11/09/15 06:22, Carter Schonwald wrote:
> Would this allow having a strict monoid instance for maybe, given the
> right hinting at the use site?
That's a fantastic idea, especially if it could be generalized to
Applicative functors, where the problem of "inner laziness" is pervasive.
But that'
Would this allow having a strict monoid instance for maybe, given the right
hinting at the use site?
On Wednesday, September 9, 2015, Edward Kmett wrote:
> I think ultimately the two views of levity that we've been talking diverge
> along the same lines as the pi vs forall discussion from your L
On 10/09/2015 10:41, Simon Peyton Jones wrote:
| > The awkward spot is the runtime system. Currently it goes to some
| > lengths to ensure that it never introduces an indirection for a
| > boxed-but-unlifted type. Simon Marlow would know exactly where. So
|
| I *think* we're ok here. The
These observations from Ed and Dan are quite helpful. Could one of you put them
on the wiki page? I hadn't considered the possibility of truly parametric
levity polymorphism.
Thanks!
Richard
On Sep 9, 2015, at 3:30 PM, Edward Kmett wrote:
> I think ultimately the two views of levity that we'v
| > The awkward spot is the runtime system. Currently it goes to some
| > lengths to ensure that it never introduces an indirection for a
| > boxed-but-unlifted type. Simon Marlow would know exactly where. So
|
| I *think* we're ok here. The RTS doesn't have any special machinery
| to av
structor.
Simon
| -Original Message-
| From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of
| Richard Eisenberg
| Sent: 08 September 2015 14:46
| To: ghc-devs
| Subject: Re: Unlifted data types
|
| I have put up an alternate set of proposals on
|
|https://ghc.haskell.
I think ultimately the two views of levity that we've been talking diverge
along the same lines as the pi vs forall discussion from your Levity
polymorphism talk.
I've been focused entirely on situations where forall suffices, and no
distinction is needed in how you compile for both levities.
May
On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg wrote:
> No functions (excepting `error` and friends) are truly levity polymorphic.
I was talking with Ed Kmett about this yesterday, and he pointed out
that this isn't true. There are a significant array of levity
polymorphic functions having to
On Sep 9, 2015, at 8:57 AM, Simon Peyton Jones wrote:
> | I mean that, for example, `length` will work over both strict lists
> | and lazy lists. It will infer the strictness of its argument through
> | ordinary type inference. So users have to be aware of strictness, but
> | they will be ab
| I mean that, for example, `length` will work over both strict lists
| and lazy lists. It will infer the strictness of its argument through
| ordinary type inference. So users have to be aware of strictness, but
| they will be able to use the same functions in both cases.
I didn't understand
On Sep 9, 2015, at 8:40 AM, Simon Peyton Jones wrote:
> Can you be more specific? What does "gloss over" mean?
I mean that, for example, `length` will work over both strict lists and lazy
lists. It will infer the strictness of its argument through ordinary type
inference. So users have to be
aving the compiler to the Right Thing during inference.
Can you be more specific? What does "gloss over" mean?
S
| -Original Message-
| From: Richard Eisenberg [mailto:e...@cis.upenn.edu]
| Sent: 09 September 2015 13:35
| To: Simon Peyton Jones
| Cc: ghc-devs
| Subject: Re
On Sep 9, 2015, at 8:28 AM, Simon Peyton Jones wrote:
> I think it'd be better to have
>
> TYPE :: TypeShape -> *
>
> data TypeShape = Unboxed | Boxed Levity
> data Levity = Lifted | Unlifted
>
Yes, of course.
> So we really would get very little levity polymorphism ineed. I think.
That'
ith Dan Doel's point about making ! a first class type
constructor.
Simon
| -Original Message-
| From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of
| Richard Eisenberg
| Sent: 08 September 2015 14:46
| To: ghc-devs
| Subject: Re: Unlifted data types
|
| I have
what happens
now.)
But if you wrote, say,
data S = MkS (!Int, !a)
then this magic would not happen and you really would get
MkS :: (!Int, !a) -> S
Interesting.
Simon
| -Original Message-
| From: Dan Doel [mailto:dan.d...@gmail.com]
| Sent: 09 September 2015 03:44
| To: Si
I would say, by the way, that your question still makes some sense.
When discussing strict evaluation, one can think of _values_ of a type
and _expressions_ of a type. The (denotational) semantics of values
would be unlifted, while expressions are lifted. And functions take
values to expressions.
On Tue, Sep 8, 2015 at 3:52 AM, Simon Peyton Jones
wrote:
> | And to
> | be honest, I'm not sure we need arbitrary data types in Unlifted;
> | Force (which would be primitive) might be enough.
>
> That's an interesting thought. But presumably you'd have to use 'suspend' (a
> terrible name) a
> Top-level variables may not have an unlifted type
Ah, that makes much more sense now. Thanks.
Janek
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
| > data unlifted UBool = UTrue | UFalse
| >
| > Intuitively, if you have x :: UBool in scope, you are guaranteed to
| > have UTrue or UFalse, and not bottom.
|
| But I still can say:
|
| foo :: UBool
| foo = foo
|
| and now foo contains bottom.
You definitely CANNOT have a top-level
On Sep 8, 2015, at 10:15 AM, Jan Stolarek wrote:
> But I still can say:
>
> foo :: UBool
> foo = foo
>
> ... Or am I missing
> something here?
I'm afraid you are. Top-level variables may not have an unlifted type, for
exactly this reason. If you were to do this on a local let, your program
I think the wiki page is imprecise when it says:
> data unlifted UBool = UTrue | UFalse
>
> Intuitively, if you have x :: UBool in scope, you are guaranteed to have
> UTrue or UFalse, and
> not bottom.
But I still can say:
foo :: UBool
foo = foo
and now foo contains bottom. I know that any a
I have put up an alternate set of proposals on
https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
These sidestep around `Force` and `suspend` but probably have other problems.
They make heavy use of levity polymorphism.
Back story: this all was developed in a late-evening Haskell Sympos
| And to
| be honest, I'm not sure we need arbitrary data types in Unlifted;
| Force (which would be primitive) might be enough.
That's an interesting thought. But presumably you'd have to use 'suspend' (a
terrible name) a lot:
type StrictList a = Force (StrictList' a)
data StrictList' a = N
| The problem 'Force' is trying to solve is the fact that Haskell
| currently has many existing lifted data types, and they all have
| ~essentially identical unlifted versions. But for a user to write the
| lifted and unlifted version, they have to copy paste their code or use
| 'Force'.
But
On Mon, Sep 7, 2015 at 5:37 PM, Simon Peyton Jones
wrote:
> But it's an orthogonal proposal. What you say is already true of Array# and
> IORef#. Perhaps there are functions that are usefully polymorphic over
> boxed-but-unlifted things. But our users have not been crying out for this
> poly
Excerpts from Simon Peyton Jones's message of 2015-09-07 14:55:09 -0700:
> I'm still doubtful. What is the problem you are trying to solve here? How
> does Force help us?
The problem 'Force' is trying to solve is the fact that Haskell
currently has many existing lifted data types, and they all
| I agree that we can't introduce a coercion between 'Force a' and
| 'a', for the reason you mentioned. (there's also a second reason which
| is that 'a ~R Force a' is not well-typed; 'a' and 'Force a' have
| different kinds.)
|
| I've imagined that we might be able to just continue representing
|
on
| -Original Message-
| From: Edward Z. Yang [mailto:ezy...@mit.edu]
| Sent: 07 September 2015 22:36
| To: Simon Peyton Jones
| Cc: ghc-devs
| Subject: RE: Unlifted data types
|
| Hello Simon,
|
| > There are several distinct things being mixed up.
|
| I've split the document into three
| Splitting # into two kinds is useful even if functions can't be levity
| polymorphic. # contains a bunch of types that aren't represented
| uniformly. Int# might be 32 bits while Double# is 64, etc. But
| Unlifted would contain only types that are uniformly represented as
| pointers, so you could
Hello Simon,
> There are several distinct things being mixed up.
I've split the document into three (four?) distinct subproposals.
Proposals 1 and 2 stand alone.
> (1) First, a proposal to allow a data type to be declared to be unlifted. On
> its own, this is a pretty simple proposal: [snip]
>
On Mon, Sep 7, 2015 at 4:00 PM, Simon Peyton Jones
wrote:
> (2) Second, we cannot expect levity polymorphism. Consider
>map f (x:xs) = f x : map f xs
> Is the (f x) a thunk or is it evaluated strictly? Unless you are going to
> clone the code for map (which levity polymorphism is there to a
| After many discussions and beers at ICFP, I've written up my current
| best understanding of the unlifted data types proposal:
|
| https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
Too many beers! I like some, but not all, of this.
There are several distinct things being mixed up.
15 16:46
| To: Eric Seidel; ghc-devs
| Subject: Re: Unlifted data types
|
| Excerpts from Edward Z. Yang's message of 2015-09-04 08:43:48 -0700:
| > Yes. Actually, you have a good point that we'd like to have functions
| > 'force :: Int -> !Int' and 'suspend :: !I
Excerpts from Dan Doel's message of 2015-09-05 10:35:44 -0700:
> I tried with `error` first, and it worked exactly the way I described.
>
> But I guess it's a type inference weirdness. If I annotate mv# with
> MutVar# it will work, whereas otherwise it will be inferred that mv#
> :: a where a :: *
Yes, I think you are right. I've restructured the spec so that 'Box'
is an optional extension.
Excerpts from Dan Doel's message of 2015-09-06 13:56:35 -0700:
> On Sat, Sep 5, 2015 at 1:35 PM, Dan Doel wrote:
> > Also, the constructor isn't exactly relevant, so much as whether the
> > unlifted er
On Sat, Sep 5, 2015 at 1:35 PM, Dan Doel wrote:
> Also, the constructor isn't exactly relevant, so much as whether the
> unlifted error occurs inside the definition of a lifted thing.
So, in light of this, `Box` is not necessary to define `suspend`. We
can simply write:
suspend :: Force a ->
On Sat, Sep 5, 2015 at 3:06 AM, Edward Z. Yang wrote:
>> If we examine an analogue of some of your examples:
>>
>> data MutVar a = MV (MutVar# RealWorld a)
>>
>> main = do
>> let mv# = undefined
>> let mv = MV mv#
>> putStrLn "Okay."
>>
>> The above is illegal. Instead we
Excerpts from Dan Doel's message of 2015-09-04 18:21:29 -0700:
> Here are some additional thoughts.
>
> If we examine an analogue of some of your examples:
>
> data MutVar a = MV (MutVar# RealWorld a)
>
> main = do
> let mv# = undefined
> let mv = MV mv#
> putStrLn "Oka
Excerpts from Dan Doel's message of 2015-09-04 14:48:49 -0700:
> I don't really understand what this example is showing. I don't think
> SPair is a legal
> declaration in any scenario.
>
> - In current Haskell it's illegal; you can only put ! directly on fields
> - If !a :: Unlifted, then (,) (!a)
Here are some additional thoughts.
If we examine an analogue of some of your examples:
data MutVar a = MV (MutVar# RealWorld a)
main = do
let mv# = undefined
let mv = MV mv#
putStrLn "Okay."
The above is illegal. Instead we _must_ write:
let !mv# = undefined
wh
If x :: t, and t :: Unlifted, then
let x = e in e'
has a value that depends on evaluating e regardless of its use
in e' (or other things in the let, if they exist). It would be like writing
let !x = e in e'
today.
-- Dan
On Fri, Sep 4, 2015 at 5:41 PM, Roman Cheplyaka wrote:
> On 05/
On Fri, Sep 4, 2015 at 5:23 PM, Edward Z. Yang wrote:
> But this kind of special handling is a bit bothersome. Consider:
>
> data SPair a b = SPair (!a, !b)
>
> The constructor has what type? Probably
>
> SPair :: (Force a, Force b) -> SPair a
>
> and not:
>
> SPair :: (a, b) -> SPair
On 05/09/15 00:41, Roman Cheplyaka wrote:
> On 05/09/15 00:23, Edward Z. Yang wrote:
>> I would certainly agree that in terms of the data that is representable,
>> there is not much difference; but there is a lot of difference for the
>> client between Force and a strict field. If I write:
>>
>>
On 05/09/15 00:23, Edward Z. Yang wrote:
> I would certainly agree that in terms of the data that is representable,
> there is not much difference; but there is a lot of difference for the
> client between Force and a strict field. If I write:
>
> let x = undefined
> y = Strict x
>
Excerpts from Dan Doel's message of 2015-09-04 13:09:26 -0700:
> Okay. That answers another question I had, which was whether MutVar#
> and such would go in the new kind.
>
> So now we have partial, extended natural numbers:
>
> data PNat :: * where
> PZero :: PNat
> PSuc :: PNat
Okay. That answers another question I had, which was whether MutVar#
and such would go in the new kind.
So now we have partial, extended natural numbers:
data PNat :: * where
PZero :: PNat
PSuc :: PNat -> PNat
A flat domain of natural numbers:
data FNat :: * where
FZer
Hello Eric,
You can't tell; the head not withstanding, `[a]` is still a lazy list,
so you would need to look at the function body to see if any extra
forcing goes on. `Force` does not induce `seq`ing: it is an obligation
for the call-site.
(Added it to the FAQ).
Edward
Excerpts from Eric Seidel
Excerpts from Dan Doel's message of 2015-09-04 09:57:42 -0700:
> All your examples are non-recursive types. So, if I have:
>
> data Nat = Zero | Suc Nat
>
> what is !Nat? Does it just have the outer-most part unlifted?
Just the outermost part.
> Is the intention to make the !a in data type
All your examples are non-recursive types. So, if I have:
data Nat = Zero | Suc Nat
what is !Nat? Does it just have the outer-most part unlifted?
Is the intention to make the !a in data type declarations first-class,
so that when we say:
data Nat = Zero | Suc !Nat
the !Nat part is now
Another good example would be
foo :: ![Int] -> ![Int]
Does this force just the first constructor or the whole spine? My guess
would be the latter.
On Fri, Sep 4, 2015, at 08:43, Edward Z. Yang wrote:
> Excerpts from Eric Seidel's message of 2015-09-04 08:29:59 -0700:
> > You mention NFData in
Excerpts from Edward Z. Yang's message of 2015-09-04 08:43:48 -0700:
> Yes. Actually, you have a good point that we'd like to have functions
> 'force :: Int -> !Int' and 'suspend :: !Int -> Int'. Unfortunately, we
> can't generate 'Coercible' instances for these types unless Coercible becomes
> po
Excerpts from Eric Seidel's message of 2015-09-04 08:29:59 -0700:
> You mention NFData in the motivation but then say that !Maybe !Int is
> not allowed. This leads me to wonder what the semantics of
>
> foo :: !Maybe Int -> !Maybe Int
> foo x = x
>
> bar = foo (Just undefined)
>
> are. Bas
You mention NFData in the motivation but then say that !Maybe !Int is
not allowed. This leads me to wonder what the semantics of
foo :: !Maybe Int -> !Maybe Int
foo x = x
bar = foo (Just undefined)
are. Based on the FAQ it sounds like foo would *not* force the
undefined, is that correct?
67 matches
Mail list logo
