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)
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
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.
1 Like
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.
2 Likes
…just as long as Haskell’s nonstrict semantics continue to be a first-class feature of the language:
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
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
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).
2 Likes
So this is rather embarrassing to admit, but I didn’t know that GHC supported and has supported UnliftedDatatypes since GHC 9.2. Let me use this to demonstrate why I believe levity should be on the arrow.
Consider this example:
data Maybe a
= Nothing
| Just a
type SMaybe :: Type -> UnliftedType
data SMaybe a
= SNothing
| SJust a
readInt :: String -> Maybe Int
readInt str = case readsPrec 0 str of
[(parse, _)] -> Just parse
_ -> Nothing
readInt' :: String -> SMaybe Int
readInt' str = case readsPrec 0 str of
[(parse, _)] -> SJust parse
_ -> SNothing
My claim is that readInt and readInt' are indistinguishable. Computations don’t evaluate into thunks, they evaluate into values. Both readInt "123" and readInt' "123" will evaluate into a value (Just 123 and SJust 123 respectively).
Instead it’s their callers that choose whether or not their computations involving readInt will be delayed. Consider these examples:
use :: Int
use = case readInt "123" of
Just int -> int
Nothing -> 0
use' :: Int
use' = case readInt' "123" of
SJust int -> int
SNothing -> 0
delay :: Bool -> Int
delay check =
let x = readInt "123"
in if check
then case x of
Just int -> int
Nothing -> 0
else 0
data BindSMaybe a = BindSMaybe (SMaybe a)
delay' :: Bool -> Int
delay' check =
let BindSMaybe x = BindSMaybe $ readInt' "123"
in if check
then case x of
SJust int -> int
SNothing -> 0
else 0
In both of these examples, the calling function chooses if it’s computation is delayed or not. However, now there’s a problem, for delay' to delay it’s computation it has to create a horrible wrapper.
There is a solution to this however. We can choose to make your data types levity polymorphic (in the true levity over laziness sense).
type LMaybe :: Type -> TYPE (BoxedRep l)
data LMaybe a
= LNothing
| LJust a
The issue is that this now has to be for very data type that is every expected to be on the right hand side of an arrow and doing this you would end up with the equivalent of levity on the arrow.
This is why I’m not keen on implementing GHC-style unlifted data in Hazy and I am much more interested in implement the levity on the arrow strict functions that I outlined here.
1 Like
When you say levity should be on the arrow, it reminds me of the demand signatures that GHC generates when it does strictness analysis on functions, but obviously Haskell doesn’t allow you to specify that in the surface syntax. So, in a way, you’re talking about bringing that to the surface syntax, but to be at parity with GHC’s demand signatures, you’d have to be able to express nested demand structure as well, and that sounds much messier than ~ Vs !.
1 Like
Is there a paper or documentation that describes this? I would be interested to read it and compare it to what I have presented here.
I’m afraid I also have a superficial understanding of what’s going on around the demand signatures, but you can see them in action with a Haskell source (NestedDemand.hs) like this:
data MyWrap = MyWrap Int
nested :: (MyWrap, Int) → Int
nested (MyWrap x,_) | x > 5 = x
nested (_,y) = y
main :: IO ()
main = print (nested (MyWrap 41,0))
And if you compile it with ghc -O3 -ddump-simpl -fforce-recomp NestedDemand.hs, you’ll see that the nested function gets annotated with Str=<1!P(1!P(1!P(L)),ML)>, which encodes the fact that our function is strict a few layers into the function argument.
Beyond that, I can only search online and point at articles like this, but I haven’t read them myself.
That is the point of unlifted types: they are eagerly evaluated.If you want to delay it you should use lifted types. It would be nice if there was an easier way to convert between the two.
1 Like
Isn’t that what Data.Elevator does?
Yes, I think this is analogous to something I noticed a while ago in Reflecting strictness in Haskell types. That article is about strictness rather than levity, but I think there is a fairly direct correspondence between them.
3 Likes
I have another argument to present.
It’s well known with higher rank types (or system-f more generally), you can perform Scott encoding to embed algebraic data into functions. This gives us a isomorphism between algebraic data and it’s encoded correspondence.
Here’s a simple example that encodes a pair of integers.
data Point = Point Int Int
newtype Point' = Point' (forall r. (Int -> Int -> r) -> r)
to (Point x y) = Point' (\f -> f x y)
from (Point' f) = f Point
However, if any of a record’s fields are strict, the correspondence is gone, since Haskell does not support strict functions (levity on the arrow), the new arguments of the function now permit bottoms.
data Point = Point !Int !Int
newtype Point' = Point' (forall r. (Int -> Int -> r) -> r)
-- not surjective, `x`, `and `y` cannot be bottom, but the function can accept bottom
to (Point x y) = Point' (\f -> f x y)
-- not injective, `f` lazily takes two arguments, but it evaluates them
from (Point' f) = f Point
This can be fixed with strict functions.
data Point = Point !Int !Int
newtype Point' = Point' (forall r. (!Int -> !Int -> r) -> r)
to (Point x y) = Point' (\f -> f x y)
from (Point' f) = f Point
Now these functions are proper bijections again. Hence the existence of strict fields hint toward the existence of strict functions and levity on the arrow, not the kind.
2 Likes
How about this:
type Strict :: Type -> UnliftedType
data Strict a = MkStrict !a
type StrictFunction :: Type -> Type -> Type
newtype StrictFunction a b = MkStrictFunction (Strict a -> b)
1 Like
(Not so) suddenly I feel vindicated / far more justified in my ‘toy’ experiments…
2 Likes
That’s possible, yes, but that’s the clunky levity on the kind encoding. I’m not arguing that it’s not possible, I’m arguing it’s less then ideal.
You could also do the same with linear types. Following from the paper I linked in the OP, here is an example that compares the by name (on the arrow) and by value (on the kind) encodings of simply typed lambda calculus into linear lambda calculus.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LinearTypes #-}
module Jaror where
import GHC.Exts
-- Unrestricted, I.E. (!) from linear logic
data U a where
U :: a -> U a
-- baseline unrestricted function
duplicate :: t1 -> (t1 -> t1 -> t2) -> t2
duplicate x f = f x x
-- the easy by name encoding of the simply typed lambda calculus into the
-- linear lambda calculus
duplicate1 :: U t1 %1 -> U (U t1 %1 -> U t1 %1 -> t2) %1 -> t2
duplicate1 (U x) (U f) = f (U x) (U x)
-- linear haskell is based off the by name encoding
duplicate1' :: t1 %Many -> (t1 %Many -> t1 %Many -> t2) -> t2
duplicate1' x f = f x x
-- the hard by value encoding of the simply typed lambda calculus into the
-- linear lambda calculus
duplicate2 :: U (U t1 %1 -> U (U (U t1 %1 -> U (U t1 %1 -> U t2)) %1 -> U t2))
duplicate2 =
U
( \(U x) ->
U
( \(U f) ->
(case (case U f of U f1 -> f1) (U x) of U f2 -> f2) (U x)
)
)
Notice how the by value encoding is significantly more clunky. You run into the same issue with levity on the kind.
Side note, I’m only using the encoding algorithm show cased in the paper. In this exact example, you could do a reduction to make the by value case a little less ugly, your still limited by the more complicated type.
1 Like