Levity should be on the arrow, not on the kind

#9

:open_mouth: I’ve done this in my own toy language and I quite like it, though I did it for other purposes and so unboxed types are always strict. I stole the idea from gulcii, which is a nice and friendly resource for low-level lambda calculus. If I recall, I used some syntax like:

foo = \ !strict &copy *lazy -> ...

That way, you could still retain the sugar for nested lambdas.

#10

Thanks, that made your proposal a lot clearer!
Using the following part of your definition:

  • ~σ -> τ
    • If σ is not lifted, then inhabitants of this type must be equivalent to \x -> e[let Shift y = x in y / x] , where Shift is some fresh shift type that wraps the unboxed value in data.

I can now see where we talked past each other. If you instantiate σ with Int# here, then you would say that an unboxed Int was passed lazily, whereas I would say that you just passed a Shift(Int#) in this function.

So I think we are now on the same page w.r.t what we mean :slight_smile: Let me put forward why I think that the idea that levity should be on the kind instead of the arrow is ultimately the better design decision.
I think there are two important questions: one is more relevant for programmers and users of the language and the other is more important for implementors and compiler writers.

Let’s start with the programmers point of view: Suppose you have discovered that your program contains a space leak, so you know that you somehow have to make your program stricter. In Haskell you currently have two possible ways to achieve that, you can either change the definition of the type or you can change the implementation of the functions which work on that type. Changing the definition means adding ! to fields or using the UnliftedDatatypes extension. Changing the implementation means inserting seq, deepseq and $! into your program. And my impression is that the majority of Haskell users nowadays prefers to change the definition of the type instead of going through all the places where it is used and forcing computation there. I think this is some sort of anecdotal evidence that programmers prefer to think of some types as always standing for fully evaluated types and other types for potentially unevaluated thunks. This leads to a design where we distinguish between StrictList and LazyList instead of thinking about functions forcing their argument or not.

The second point is more relevant for implementors than users: The question is when you are allowed to eta-expand a function f : a -> b -> c to its expanded form \x y. f x y. This is the main content of the “Kinds are calling conventions” paper that @Jaror cited above. We know pretty well how to do that for the levity-on-the-kind approach, but you would have to check whether you can have an equally good story for the levity-on-the-arrow approach that you propose.

2 Likes
#11

Alright, so this post is about levity polymorphism: having definitions that can use both e.g. Int (lifted) and Int# (unlifted)…

o_0 …this thread is no longer about (just) levity polymorphism, there’s been some “scope creep” - now it seems to me that you’re contemplating changing laziness from being implicit (part of the language) to being explicit (e.g. described as a type, kind, sort et al ) - that changes matters for a language like Haskell substantially.

I suggest reading and watching the following:

Of course, I’m not suggesting that you should use implicit laziness in your own language, and from this description:

…implicit laziness probably would be “out of place” - it seems yours could be used as an intermediate language, and most of those are usually strict by default (as I vaguely recall, the “types are calling conventions” paper was also contemplating a strict-by-default intermediate language for GHC). So in that respect you’re not alone in seeking a smaller/simpler (faster?) typed functional language…or building your own.

#12

Let me quote the original paper:

In general, a boxed value is represented by a pointer into the heap, while an unboxed value is represented by the value itself.
…
Haskell also requires consideration of levity—that is, the
choice between lifted and unlifted. A lifted type is one that is
lazy.

Levity polymorphism is about adding the ability to reason about types that aren’t lifted (levity) and types that aren’t boxed (representation) to Haskell. What my post is about is how I believe an alternative way to reason about levity would be superior. It feels pretty in scope to me.

It wouldn’t be a bigger change the what levity polymorphism already is. Of course if my proposal was to actually be implemented -> would still be lazy by default. seq would still work and still be a -> b -> b. Bang pattern would still not change the type system. I’m not suggesting Haskell stop being lazy by default or anything.

The only real breaking change would be that now unboxed types would need to use strict arrows to avoid being passed lazily. So like Int# -> ... would now need to be !Int# -> ....

2 Likes
#13

So instead of:

(->) (RawType#) (...)

as it is now, an unlifted and strictly-used parameter would instead require:

(!->) (RawType#) (...)

But as you mentioned linear parameters earlier: what if someone needs a parameter to be both linear and strict (e.g. State# RealWorld)? Presumably it wouldn’t be possible to use both (%1->) and (!->) simultaneously for the exact same parameter…

#14

Why wouldn’t you be able to? Just make function arrows have 4 parameters: levity, multiplicity, argument, and result.

#15

There’s an old strict dialect of Haskell that used to be called Disciple (now called Discus) which did something similar - from this old page on the Haskell wiki:

map  :: forall a b %r0 %r1 !e0 $c0
     .  (a -(!e0 $c0)> b) -> List %r0 a -(!e1 $c1)> List %r1 b
     :- !e1        = !{ !Read %r0; !e0 }
     ,  $c1        = f : $c0

…fortunately that particular signature could be simplified to:

map :: (a -> b) -> [a] -> [b]

due to Disciple’s type-elaboration mechanism. So if (that style of) type elaboration could be brought into Haskell so that people didn’t have to perpetually “hammer out” :

  • ... -> ...
  • ... %1 -> ...
  • ... !%1 -> ...
  • ... %n -> ...
  • ... !%n -> ...

etc, throughout all of their code…then maybe it could work. But this poses another question - why was Disciple (now Discus) abandoned?

#16

Isn’t levity and lazyness fundamentally different? As I understand it, Int# as opposed to Int is a type that has no bottom. There is the embedding I# :: Int# -> Int. Observe that there is no map going the reverse way. In contrast, given any lifted type T with lazy fields, one can define a stricter variant T' by adding bangs to the fields. This defines a quotient map q :: T -> T' which has a left adjoint. An extreme example:

import Data.Void (Void, absurd)
data Nat = Succ Nat
-- Succ lifts any value one level higher
q :: Nat -> Void
q (Succ n) = q n
-- Void ~ Succ !Void

We have q . absurd = id and absurd . q ⊑ id.
Thus more or less strict types are related by embedding-projection pairs while boxed and unboxed types are only related by an embedding.
We might express lazyness of a function by a factoring through a stricter type. E.g. the function f = const () :: Nat -> () is fully lazy because it factors through q. That is,

f = (absurd :: Void -> ()) . q
#17

There is a map that goes the other way, simply unpack the int…

unpack :: Int -> Int#
unpack (I# x) = x

I agree that “strict fields” and “unlifted types” are different, but I wouldn’t equate laziness with types having no strict fields.

1 Like
How many kinds of bottom are there in GHC?
#18

That’s the current status quo, but let me reiterate:

First off, let me preface this with how Int would be defined under my system. When you seq an Int you would expect to not have any thunks inside whatsoever. So the constructor of I# must be strict. If you imagine a hypothetical scenario where Int# is user defined, then you would expect the same strict fields there too.

data Int = I# !(Int#)

Lets consider the isomorphism. Since the field is strict, the construction (to) arrow can be strict without losing any expressivity and since you have the immediately pattern match on your argument the destruction arrow (from) can also be strict without losing expressivity.

to :: !Int# -> Int
from :: !Int -> Int#

For strict arrows f ⊥ = ⊥, so under my system. Int and Int# would be truly isomorphic. They would only differ in their kinds.

I haven’t studied enough category theory to understand adjoins yet, but my post isn’t really concerned with strict fields. It’s about moving top level levity to arrows.

1 Like
#19

There it is:

That’s why I refer to what Linear Haskell currently offers as being linear parameters (not types), and sometimes those aren’t enough - for example:

separates the linearity annotation from the function type (as strictness annotations for types have always been in Haskell). So to then “reverse that course” for strictness - having strict parameters (not types) - seems counterintuitive…

#20

You can still define a bottom of type !Int but writing one of type Int# is more tricky, as we see below.

{-# LANGUAGE MagicHash #-}
import GHC.Exts (Int#)
data BangInt = I !Int#
bot :: BangInt
bot = bot

botUnlifted :: Int#
botUnlifted = botUnlifted
-- error: Top-level bindings for unlifted types aren't allowed

So it seems your function from can not be implemented, since there is no value you can map bot to.

You don’t need to know category theory to grasp adjoints. What you need to know is the specialisation order ⊑ (a partial order) in which ⊥ is the least element in any lifted type and x ⊑ y whenever for any function f, if f(x) yields a value z (and does not diverge), f(y) evaluates to z as well. You can also interpret x ⊑ y as “x is a thunk that when forced might become y.” This order can be defined on every Haskell type, lifted or not. The order on Int# coincides with equality. Every definable function is monotone in this order. This is why there is no from: Since from must be monotone and ⊥ is the least element, the value from ⊥ must be below every other element in Int#, but the latter type has no such element.
This seems to contrast the unpack function @jaror has defined above, and indeed calling unpack on ⊥ results in a type error at runtime in GHCi! It really should not be definable in the first place. Can we say that GHC as the Haskell implementation has two kinds of ⊥? There is the domain-theoretic divergence ⊥ as in bot = bot and the RTS run-time type error ⊥ which is equivalent to the first one in the sense of “does not yield a value” but which other Haskell implementations might not have due to better type-checking. Funnily enough, GHCi can type the expression

(let bot = bot :: Int in unpack bot) :: Int#

but it refuses to bind this expression to a name:

botUnlifted = let bot = bot :: Int in unpack bot
-- error:
-- can't bind a variable of unlifted type: botUnlifted :: Int#

So I think what you are proposing is an annotation expressing that functions restrict to certain sub-types. For every type T, the set T \ {⊥} is a sub-type that may or may not be definable in Haskell. For any function f: X → Y you can ask whether f restricts to a function X \ {⊥} → Y \ {⊥}, or whether the pre-image of Y \ {⊥} under f is contained in X \ {⊥}.

1 Like
#21

You can do it if you put another let around it:

let botUnlifted = let bot = bot :: Int in unpack bot in ()

(But this expression is itself bottom)

#22

That term is typed as (), but you are right, inside it, botUnlifted has type Int#. I spun off the discussion of such bottoms to another thread.

1 Like
#23

I haven’t read the whole discussion, but note that Kinds are Calling Conventions as pointed out by @jaror subsumes the old notion of levity polymorphism (which really was representation polymorphism, as you point out). You should rather compare your approach to theirs.

Also from reading your proposal it is far from clear why you must annotate arrows with levity rather than just encode levity in the argument kind. Arguably, (->) (which is implemented as FUN) is already parameterised over levity today in this sense: ![a] -> b is the same as FUN @UnliftedType @Type @Many @(Strict [a]) @b, with Strict from here: Data.Elevator. The implementation mechanism of data-elevator is probably broken, but it should be possible to implement it first-class in GHC.

The only thing that isn’t currently supported is the sort of autoboxing that you allude to with ~Int#. It’s arguably a bit hard to see how that would be useful in practice, though, consider for example:

f1 :: Int# -> Int# -> Int#
f1 x y = multiply''' 42# (x /# y)

f2 :: Int# -> Int# -> Int#
f2 x y = multiply''' 42# z where z = x /# y

Does f1 allocate a thunk for x /# y? Does f2? If the answer is not the same, I would be quite upset; introducing let bindings locally should IMO be a semantics-preserving transformation.

I sympathise with wanting a great story for levity polymorphism, so that Haskell can be regarded a strict programming language. But the challenge isn’t really surface syntax, so much as enabling zero-cost coercions from Unlifted to Lifted, enabling code reuse of huge swaths of lifted-only code (perhaps by type class specialisation of an automated LevityCoercible type class instance) and implementing existing ideas in GHC Core and STG in a way that doesn’t make the whole compiler twice as complex. In fact, the latter is a prerequisite to make progress on anything involving the surface language.

#24

Oh, I should have read one more post than I did. Here you define

newtype Arrow (s :: Levity) a b = Arrow (a -> b)

strict :: (a -> b) -> Array Unlifted a b
strict f = Arrow $ \x -> f $! x

lazy :: (a -> b) -> Arrow Lifted a b
lazy f = Arrow f

and claim that strict turns a … function into an unlifted arrow. But a strict function is not a function taking an unlifted argument!

Perhaps we should first clarify what “unlifted” means. An unlifted element (of a type, say) cannot contain ⊥ (read: arbitrary code in thunks). If it did, it would be lifted; this is the definition of a lifted domain.

Claiming that strict (which makes an arbitrary function strict) produces a function taking an unlifted argument is a bit like claiming that head :: [a] -> a is the same as head1 :: NonEmpty a -> a when I promise to only call it on non-empty lists.
The difference is in the domain of the functions’ definition.

Although let f x = x+1 in strict f returns something that will never call f with a lifted argument, the code that the compiler generates for f still needs to account for the fact that x might be a thunk! In practice, this means that there will be an indirect call to x to evaluate it.
By contrast, f (x :: Strict Int) = x + 1 does not need an indirect call to evaluate x, because it is a precondition that x is evaluated. This is the beauty of types: types encode preconditions, and the r in TYPE r kinds encode preconditions that the compiler is interested in to generate code.

1 Like
#25

…just as long as Haskell’s nonstrict semantics continue to be a first-class feature of the language:

#26

Maybe I missed some specific section, but I don’t see how linear let separates linearity from the function type. In fact I see it as as another parallel between linear types and my system.

Monomorphic let is derived from creating a lambda and intimidate calling it let x = e in e' ~> (\x -> e')(e). The issue is that, on a syntax level, there’s no easy way to tell if the lambda’s parameter is linear or not and you can’t rely on the type of the lambda because it’s being immediatly called. So you probably want to annotate the linearity on bindings to aid readability and possibly type inference. In short, linearity on arrows implies linearity on bindings.

All of this applies to levity on the arrow too. Given a immediate application (\x -> e') (e), the situation is even worse then the linear type scenario as both strict and lazy would always be valid and again, you can’t rely on the function type because it’s immediately called. What you would need is a way to annotate that a binding is lazy vs strict. let x = e in ... vs let !x = e in .... So again, strictness on arrows implies strictness on bindings. Fortunately the strict let parallel to linear type’s linear let is already implemented in GHC as bang patterns.

Side note, yet another parallel is that how bindings are handled globally. You can’t have (easily) have linear globals bindings because globals are let bindings without a body and in the same sense you can’t (easily) have unlifted globals bindings because global are let bindings without an evaluation order.

1 Like
#27

This depends on whether you think a term’s type enough info to know if you should pass it lazily or not. If so, then the status quo (levity on the kind) is ideal, otherwise then you would levity on the arrow. In my opinion, if there was some idealized Haskell, where representation polymorphism is everywhere, then you frequently want to pass unboxed values lazily.

Yes, and Yes. For f1, since multiply''' is lazy in it’s second argument, f1 would allocate a thunk when it passes x /# y. For f2, since let bindings are lazy by default in Haskell z would allocate a thunk and it wouldn’t evaluate it as, again, multiply''' takes it’s second argument lazily.

Okay, so I probably implemented it incorrectly. I was unaware of Data.Elevator. Perhaps a proper implementation of userland boxed strict arrows would use Strict a.

newtype StrictArrow a b = StrictArrow (Strict a -> b)
1 Like
#28

Well, I prefer strictness for types rather than just parameters, in the same way e.g. Clean or Single-Assignment C have uniqueness for types rather than just parameters - as I explained here:

…only having linearity for parameters (but not types) isn’t always enough - I would expect that having only strictness for parameters (but not types) will invariably encounter similar problems.

In summary: to me, moving strictness from types to parameters goes against the DRY principle - rather that placing the strictness annotation only on the type declaration (best case), all functions which use that type would need their signatures annotated (worst case).

1 Like