Levity should be on the arrow, not on the kind

#1

In Levity Polymorphism a principled way to represent unboxed strict is introduced and personally, I think it’s brilliant. Levity polymorphism is something I’ve deeply integrated into Aith, my programming language. However, I’m now of the opinion that only the representation polymorphism fragment is ideal and that levity itself (whether a term is strict or not) should be on the arrow similar to linear types.

For any given type there’s one to natural way to represent it’s values. For example: for Int#, it’s values are represented with machine words, while for [a] it’s values are represented with a pointer. However, how values are represented doesn’t give the full picture of how they should be passed to functions. You could easily imagine a scenario where you have an unboxed value you want to pass lazily or a boxed value you want to pass strictly. So there’s no natural way to represent how a type should be passed to functions, so using kinds for (as is done) in levity polymorphism is less then ideal.

Lets take this example function:

multiply :: Int# -> Int# -> Int#
multiply 0# _ = 0#
multiply x y = x *# y

Since the there are cases where the second argument isn’t used, it’s plausible to want to pass it in with call by need or even call by name.

multiply' :: Int# -> Int -> Int#
mulitply' 0# _ = 0#
multiply' x (I# y) = x *# y

multiply'' :: Int# -> (() -> Int#) -> Int#
multiply'' 0# _ = 0#
multiply'' x y = x *# y()

It would be nice if we could say that the second argument is a lazy but with values that are machine ints while the first argument a normal plain strict machine int argument.

Lets imagine that function arrows are parameterized by what they want the strictness of their arguments to be. Where ~σ -> τ is a normal haskell function and !σ -> τ is a function arrow that expects it’s argument to be in whnf. The example can now be written as:

multiply''' :: !Int# -> ~Int# -> Int#
multiply''' 0# _ = 0#
multiply''' x y = x *# y

This definition would effectively be isomorphic to multiply'.

I can imagine some {-# Language StrictTypes #-} extension that allows you parameterize functions with strictness in a similar manner that {-# Language LinearTypes #-} allow you to parameterize functions with linearity. Putting aside representation polymorphism for a minute, such an extension would be very useful. It would bring some much need ability to reason about strictness in the type system.

Lastly, there’s likely some theory behind this. In Call-by-name, call-by-value, call-by-need, and the linear lambda calculus it’s explained that there’s two different ways to embed unrestricted types into linear types. One corresponding to call by name and one corresponding to call by value. If you squint at the call by name encoding, it corresponds very closely to how you would embed lazyness into a strict language.

name-crop-1
name-crop-11000×767 17 KB

for completeness here’s a similar translation of the by value encoding:
value-crop-1
value-crop-1927×1000 24 KB

In some sense, the by name encoding corresponds to parameterizing arrows while the by value encoding corresponds to parameterizing the kinds. Since GHC already has the by name encoding of linear types, why not go with the by name encoding of lazyness too?

5 Likes
How many kinds of bottom are there in GHC?
#2

I guess this must be a typo, but I can’t work out what for.

#3

Fixed, my apologies. I wrote this out of order so I had to do bit of editing.

1 Like
#4

I don’t think that it is possible to say that an unboxed Int can be passed strictly or lazily. The definition of a strict function is as follows: The function f : a -> b is strict if f ⊥ = ⊥. But for this definition to make sense in the first place it is important that ⊥ is part of the denotation of the type a, but it clearly isn’t for unboxed Ints. So if you want an unboxed Int to be passed lazily you have to “lift” it into some type which contains ⊥ in its denotation, and this is precisely what the data Int = Int Int# does. (The idea goes back to https://www.microsoft.com/en-us/research/wp-content/uploads/1991/01/unboxed-values.pdf I believe). This kind of definition is a special case of type constructors which are known as “shifts”, since they change the kind of the type they are wrapping. They are also an important part of Levy’s Call-by-push-value calculus; I like the definition given in this paper by Paul and Zena: https://pauldownen.com/publications/csl18_long.pdf

4 Likes
#5

There is also a newer paper: Kinds are calling conventions. Although, I don’t know exactly how it differs from that levity polymorphism paper.

4 Likes
#6

But for this definition to make sense in the first place it is important that ⊥ is part of the denotation of the type a

This is what I’m arguing against. Reasoning about whether a type has ⊥ is less then ideal, rather it’s better to reason about whether or not the arrow takes an argument lazily or strictly. When talking about the inhabitants of a type, it’s better to only think about the values (whnf terms).

Also, undefined is already levity polymorphic. So you can already pass ⊥ to any function that takes unboxed types.

They are also an important part of Levy’s Call-by-push-value calculus

Call by push value is something I’ve been meaning to look into but I haven’t gotten around to it yet. So I can’t really compare my idea to it.

1 Like
#7

Then maybe I don’t fully understand your proposal yet. Could you give an example of a function which takes a unboxed Int argument lazily? I don’t see how such an example is possible. But maybe the unboxed Ints are a red herring, and it works better if we use lists as an example, so that you could have ![Int] -> Int and ~[Int] -> Int, where the ! and ~ are parts of the function arrow?

Btw, I really like the direction of your language. I guess you also pursue this ideal of a low-level purely functional programming language that is hidden behind a lot of clutter in Haskell :smiley:

1 Like
#8

Then maybe I don’t fully understand your proposal yet.

If you want to think of it in terms of status quo.

  • !σ -> τ
    • If σ is lifted, then inhabitants of this type must be equivalent to \x -> f $! x, for some function f.
    • If σ is not lifted, then nothing changes. It behaves the same as current GHC.
  • ~σ -> τ
    • If σ is lifted, then do nothing. It behaves the same as current GHC.
    • 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. Basically, ~σ -> τ wraps it into something equivalent of Shift σ -> τ.

so that you could have ![Int] -> Int and ~[Int] -> Int , where the ! and ~ are parts of the function arrow?

Yes. If σ is boxed, then you can easily define !σ -> τ with current Haskell.

module Strict ( Strictness(..), Arrow, strict, lazy, call) where

data Levity = Lifted | Unlifted 

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

call :: Array s a b -> a -> b
call (Arrow f) a = f a

Btw, I really like the direction of your language. I guess you also pursue this ideal of a low-level purely functional programming language that is hidden behind a lot of clutter in Haskell

Thank you. It’s not really usable yet as it doesn’t have proper documentation, user defined data types, and other much needed functions. I’m also not sure if what direction to take it in. Like, whether I should make it into my personal research language or to actually get users.

#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