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.
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
…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).
1 Like