... | ... | @@ -13,10 +13,15 @@ See also [UnpackedSumTypes](unpacked-sum-types). |
|
|
## Motivation
|
|
|
|
|
|
|
|
|
|
|
|
Bob Harper [ has written](https://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/):
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Haskell suffers from a paucity of types. It is not possible in Haskell to define the type of natural numbers, nor the type of lists of natural numbers (or lists of anything else), nor any other inductive type!
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
The reason, of course, is that whenever you write `data Nat = Z | S !Nat`, you define a type of strict natural numbers, AS WELL AS bottom. Ensuring that an `x :: Nat` is never bottom requires all use-sites of this type to do strict pattern matching / force the value appropriately. It would be nice if there was some type-directed mechanism which specified that a value `x` was always evaluated. This would give benefits, e.g. for code generation, where we can assume that a pointer never points to a thunk or indirection.
|
... | ... | @@ -30,52 +35,76 @@ The fact that a pointer never points to a thunk is especially helpful in the imp |
|
|
## Proposal 1: Allow data types to be declared as unlifted
|
|
|
|
|
|
|
|
|
|
|
|
A data type can be declared as unlifted by writing `data unlifted`, e.g.:
|
|
|
|
|
|
|
|
|
```
|
|
|
data unlifted UBool=UTrue|UFalse
|
|
|
data unlifted UBool = UTrue | UFalse
|
|
|
```
|
|
|
|
|
|
|
|
|
Such data types are always boxed, but the type does not include bottom and is operationally represented as a pointer to the value. Intuitively, if you have `x :: UBool` in scope, you are guaranteed to have `UTrue` or `UFalse`, and not bottom.
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> **Iceland_jack**: Yakshaving, to avoid new syntax we can use `GADTSyntax` and write
|
|
|
>
|
|
|
>
|
|
|
> ```
|
|
|
> dataUBool::TYPEUnliftedRepwhereUFalse::UBoolUTrue::UBool
|
|
|
> data UBool :: TYPE UnliftedRep where
|
|
|
> UFalse :: UBool
|
|
|
> UTrue :: UBool
|
|
|
> ```
|
|
|
|
|
|
|
|
|
|
|
|
The evaluation rules for unlifted data types are identical to the existing rules we have for types kinded `#`: lets are strict, cannot be recursive, and function arguments are evaluated before calls. For example:
|
|
|
|
|
|
|
|
|
```
|
|
|
unot::UBool->UBoolunotUTrue=UFalseunotUFalse=UTruemain::IO()main=let y = unot (error"foo")in return ()
|
|
|
unot :: UBool -> UBool
|
|
|
unot UTrue = UFalse
|
|
|
unot UFalse = UTrue
|
|
|
|
|
|
main :: IO ()
|
|
|
main = let y = unot (error "foo")
|
|
|
in return ()
|
|
|
```
|
|
|
|
|
|
|
|
|
In this example, we get the error "foo", rather than returning `()`, because the binding of `y` must be evaluated strictly.
|
|
|
|
|
|
|
|
|
|
|
|
Just like other unlifted types, you cannot bind values of an unlifted data type at top level, or in a recursive group. So this is illegal
|
|
|
|
|
|
|
|
|
```
|
|
|
moduleMwheredata unlifted UBool=UTrue|UFalse
|
|
|
module M where
|
|
|
data unlifted UBool = UTrue | UFalse
|
|
|
|
|
|
utrue ::UBool
|
|
|
uTrue =UTrue-- Illegal!
|
|
|
utrue :: UBool
|
|
|
uTrue = UTrue -- Illegal!
|
|
|
```
|
|
|
|
|
|
|
|
|
**Non-polymorphic unlifted types can directly be unpacked.** The following declaration is valid:
|
|
|
|
|
|
|
|
|
```
|
|
|
data unlifted StrictInt=StrictIntInt#dataMyInt=MyInt{-# UNPACK #-}StrictInt
|
|
|
data unlifted StrictInt = StrictInt Int#
|
|
|
data MyInt = MyInt {-# UNPACK #-} StrictInt
|
|
|
```
|
|
|
|
|
|
|
|
|
and is representationally equivalent to `MyInt'` here:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataInt=IntInt#dataMyInt'=MyInt'{-# UNPACK #-}!Int
|
|
|
data Int = Int Int#
|
|
|
data MyInt' = MyInt' {-# UNPACK #-} !Int
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -87,31 +116,45 @@ Of course, the constructors for `MyInt` and `MyInt'` have different types. |
|
|
Currently, we have two different kinds (ahem) of unlifted types which live in `#`: unboxed, unlifted types such as `Int#`, and boxed, unlifted types such as `Array#` and the unlifted data types we can now define.
|
|
|
|
|
|
|
|
|
|
|
|
This subproposal is to distinguish between these two kinds, calling boxed, unlifted kinds `Unlifted`. If users start defining and using unlifted types in normal code, it is likely that they will request polymorphism over unlifted types. There are two particular cases of polymorphism we might like to support:
|
|
|
|
|
|
|
|
|
|
|
|
**Polymorphism over unlifted types in types and functions.** In data types and functions, we may want to be polymorphic over a type variable in kind `Unlifted`:
|
|
|
|
|
|
|
|
|
```
|
|
|
data unlifted UList(a ::Unlifted)=UNil|UCons a UListumap:: forall (a ::Unlifted)(b ::Unlifted).UList a ->(a -> b)->UList b
|
|
|
data unlifted UList (a :: Unlifted)
|
|
|
= UNil | UCons a UList
|
|
|
umap :: forall (a :: Unlifted) (b :: Unlifted).
|
|
|
UList a -> (a -> b) -> UList b
|
|
|
```
|
|
|
|
|
|
|
|
|
We cannot be polymorphic in `#` in general, because this includes unboxed types like `Int#` which don't have uniform representation. However, we can be polymorphic over unlifted types, which do have uniform representation.
|
|
|
|
|
|
|
|
|
|
|
|
**Boxed levity polymorphism in types (and functions with extra code generation).** In data types, we may want to have a type parameter which is polymorphic over all boxed types:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataBList(a ::Boxed)=BNil|BCons a BList
|
|
|
data BList (a :: Boxed)
|
|
|
= BNil | BCons a BList
|
|
|
```
|
|
|
|
|
|
|
|
|
`BList` is representationally the same whether or not it is instantiated with a boxed lifted type, or a boxed unlifted type.
|
|
|
|
|
|
|
|
|
|
|
|
However, for levity polymorphism over functions we must generate code twice. Consider::
|
|
|
|
|
|
|
|
|
```
|
|
|
map:: forall a (b ::Boxed).(a -> b)->BList a ->BList b
|
|
|
map f (BCons x xs)=BCons(f x)(map f xs)
|
|
|
map :: forall a (b :: Boxed). (a -> b) -> BList a -> BList b
|
|
|
map f (BCons x xs) = BCons (f x) (map f xs)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -120,42 +163,69 @@ We do not know if `f x` should be evaluated strictly or lazily; it depends on wh |
|
|
## Proposal 3: Allow newtypes over unlifted types
|
|
|
|
|
|
|
|
|
|
|
|
To allow cost-free abstraction over unlifted types, we should allow newtypes to be written over types of kind `#`, with the resulting newtype being in kind `#`. For example:
|
|
|
|
|
|
|
|
|
```
|
|
|
newtypeMyInt#=MkInt#Int#
|
|
|
newtype MyInt# = MkInt# Int#
|
|
|
```
|
|
|
|
|
|
|
|
|
with `MyInt# :: #`. GHC already supports coercions over kind `#`, so this should be very simple to implement.
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> **Iceland_jack**: Use this to wrap `Int#` when used in boolean context in `GHC.Exts`, `GHC.Prim`
|
|
|
>
|
|
|
>
|
|
|
> ```
|
|
|
> newtypeBool#=Bool#Int#patternFalse#::Bool#patternFalse#=Bool0#patternTrue#::Bool#patternTrue#=Bool1#(==#)::Int#->Int#->Bool#(==##)::Double#->Double#->Bool#
|
|
|
> newtype Bool# = Bool# Int#
|
|
|
>
|
|
|
> pattern False# :: Bool#
|
|
|
> pattern False# = Bool 0#
|
|
|
>
|
|
|
> pattern True# :: Bool#
|
|
|
> pattern True# = Bool 1#
|
|
|
>
|
|
|
> (==#) :: Int# -> Int# -> Bool#
|
|
|
> (==##) :: Double# -> Double# -> Bool#
|
|
|
> ```
|
|
|
>
|
|
|
>
|
|
|
> and other similar cases.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
## Proposal 4: Allow unlifting existing data types with no overhead
|
|
|
|
|
|
|
|
|
|
|
|
Proposal 1 requires a user to define a new data type for every unlifted type they want to define. However, for every lifted data type a user can define, there is an obvious unlifted type one might be interested in: the one without bottom. Fortunately, we can define a data type to unlift an arbitrary lifted type:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataForce::*->UnliftedwhereForce::!a ->Force a
|
|
|
data Force :: * -> Unlifted where
|
|
|
Force :: !a -> Force a
|
|
|
|
|
|
suspend::Force a -> a
|
|
|
suspend :: Force a -> a
|
|
|
suspend a = a
|
|
|
```
|
|
|
|
|
|
|
|
|
`Force a` is the "head strict" version of `a`: if you have `x :: Force Int` in scope, it is guaranteed to have already been evaluated to an `Int`. We can also suspend these strict computations: `suspend (error "foo" :: Int#)` does not error until forced. Like `Box`, unlifted computations may not be lifted out of `suspend` without changing the semantics.
|
|
|
|
|
|
|
|
|
|
|
|
`Force` and `suspend` can be written purely as library code, however there is a cost of an indirection of `Force`. We might notice, however, that the value of type `Force a` only admits the value `Force a`: `undefined` is excluded by the `Unlifted` kind, and `Force undefined` is excluded by the strict field. Thus, it would be great if we could represent `Force` on the heap simply as an unlifted pointer to `a`, which is never undefined.
|
|
|
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> Note from David Feuer: the indirection problem could be resolved via [ https://ghc.haskell.org/trac/ghc/wiki/NewtypeOptimizationForGADTS](https://ghc.haskell.org/trac/ghc/wiki/NewtypeOptimizationForGADTS), which would be a good thing for other reasons too.
|
|
|
>
|
|
|
>
|
|
|
|
|
|
|
|
|
Ideally, we would like to define the coercion `Coercible (Force a) a`, to witness the fact that `Force a` is representationally the same as `a`. However, there are two problems:
|
... | ... | @@ -167,36 +237,51 @@ Ideally, we would like to define the coercion `Coercible (Force a) a`, to witnes |
|
|
|
|
|
My suggested implementation strategy is to bake in `Force` as a special data type, which is represented explicitly in Core, but then optimized away in STG.
|
|
|
|
|
|
|
|
|
## Optional extensions
|
|
|
|
|
|
|
|
|
|
|
|
**(OPTIONAL) Give some syntax for `Force`.** Instead of writing `f :: Force Int -> Force Int`, we might like to write `f :: Int! -> Int!`. We define post-fix application of bang to be a wrapping of `Force`.
|
|
|
|
|
|
**(OPTIONAL) Introduce a pattern synonym `Thunk`.**`suspend` can be generalized into the bidirectional pattern synonym `Thunk`:
|
|
|
|
|
|
|
|
|
**(OPTIONAL) Introduce a pattern synonym `Thunk`.** `suspend` can be generalized into the bidirectional pattern synonym `Thunk`:
|
|
|
|
|
|
|
|
|
```
|
|
|
patternThunk a <- x |let a =Force x
|
|
|
whereThunk(Force a)= a
|
|
|
pattern Thunk a <- x | let a = Force x
|
|
|
where Thunk (Force a) = a
|
|
|
```
|
|
|
|
|
|
>
|
|
|
>
|
|
|
> **Iceland_jack**: This syntax is invalid, is this what was intended?
|
|
|
>
|
|
|
>
|
|
|
> ```
|
|
|
> pattern::Force a -> a
|
|
|
> patternThunk a <-(Force-> a)whereThunk(Force a)= a
|
|
|
> pattern :: Force a -> a
|
|
|
> pattern Thunk a <- (Force -> a)
|
|
|
> where Thunk (Force a) = a
|
|
|
> ```
|
|
|
|
|
|
|
|
|
|
|
|
For example:
|
|
|
|
|
|
|
|
|
```
|
|
|
let x =Thunk(error"foo"::ForceInt)::IntinTrue
|
|
|
let x = Thunk (error "foo" :: Force Int) :: Int
|
|
|
in True
|
|
|
```
|
|
|
|
|
|
|
|
|
does not error. Pattern matching over `Thunk` forces the argument (similar to bang patterns) and returns the unlifted value (unlike bang patterns):
|
|
|
|
|
|
|
|
|
```
|
|
|
letThunk x =3+5::Intin x ::ForceInt
|
|
|
let Thunk x = 3 + 5 :: Int
|
|
|
in x :: Force Int
|
|
|
```
|
|
|
|
|
|
## Dynamic semantics of unlifted types
|
... | ... | @@ -213,31 +298,48 @@ In this section, we review the dynamic semantics of unlifted types. These are n |
|
|
**Constructors and function application.** Given `K e` where `e` is `Unlifted`, this desugars into `case e of !x -> K x`. NB: if `K` is in kind star, then this expression admits bottom!
|
|
|
|
|
|
|
|
|
|
|
|
Intuitively, if you have an unlifted type, anywhere you let bind it or pass it to a function, you evaluate it. Strict let bindings cannot be arbitrarily floated; you must preserve the ordering of bindings and they cannot be floated beyond an expression kinded `*`.
|
|
|
|
|
|
|
|
|
## FAQ
|
|
|
|
|
|
**Why do you get to use error in the unlifted examples, isn't error a bottom?**`error` is specially treated to be both lifted and unlifted. It's interpretation in an unlifted setting is that it immediately causes an exception when it is evaluated (it never goes into the heap).
|
|
|
|
|
|
|
|
|
**Why do you get to use error in the unlifted examples, isn't error a bottom?** `error` is specially treated to be both lifted and unlifted. It's interpretation in an unlifted setting is that it immediately causes an exception when it is evaluated (it never goes into the heap).
|
|
|
|
|
|
|
|
|
|
|
|
**Why not `!Int` rather than `Int!` as the syntax proposal?** This syntax conflicts with strict data fields. `data S a = S !a` has a constructor of type `S :: Int -> S`, taking a lifted type and evaluating it before placing it in the constructor; `data S a = S a!` has a constructor of type `S :: Force Int -> S`, which requires the *user* to have forced the integer. Representationally, the data types are the same, but the outward behavior for clients differs dramatically.
|
|
|
|
|
|
|
|
|
|
|
|
**Is `Force (Maybe (Force Int))` allowed?** No, because `Force Int` has kind `Unlifted` but `Maybe` has kind `* -> Unlifted`. A data type declaration must be explicitly written to accept an unlifted type (`data StrictMaybe (a :: Unlifted) = SMaybe a`), or simply be strict in its field (`data StrictMaybe2 a = SMaybe2 !a`).
|
|
|
|
|
|
|
|
|
|
|
|
**How does this affect inlining?** In any CBV language, inlining doesn't always preserve semantics; unlifted types are no different. For example, this errors:
|
|
|
|
|
|
|
|
|
```
|
|
|
let x =error"foo"::ForceInt
|
|
|
y = suspend x ::IntinTrue
|
|
|
let x = error "foo" :: Force Int
|
|
|
y = suspend x :: Int
|
|
|
in True
|
|
|
```
|
|
|
|
|
|
|
|
|
but this example does not:
|
|
|
|
|
|
|
|
|
```
|
|
|
let y = suspend (error"foo"::ForceInt)::IntinTrue
|
|
|
let y = suspend (error "foo" :: Force Int) :: Int
|
|
|
in True
|
|
|
```
|
|
|
|
|
|
**What's the difference between `Force Int` and `Int#`?**`Force Int` is an unlifted, boxed integer; `Int#` is an unlifted, unboxed integer.
|
|
|
|
|
|
**What's the difference between `Force Int` and `Int#`?** `Force Int` is an unlifted, boxed integer; `Int#` is an unlifted, unboxed integer.
|
|
|
|
|
|
|
|
|
|
|
|
**Why aren't strict patterns enough?** A user can forget to write a strict pattern at a use-site. Putting a type in kind unlifted forces all use-sites to act as if they had strict patterns.
|
|
|
|
... | ... | @@ -253,21 +355,40 @@ This section describes a totally alternate proposal to the one(s) above. The mot |
|
|
## Proposal B1. Allow newtypes over unlifted types
|
|
|
|
|
|
|
|
|
|
|
|
Identical to Proposal 3 above.
|
|
|
|
|
|
|
|
|
## Proposal B2. More levity polymorphism
|
|
|
|
|
|
|
|
|
|
|
|
[NoSubKinds](no-sub-kinds) proposes the following arrangement:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataLevity=Lifted|UnliftedTYPE::Levity->*type*=TYPE'Liftedtype#=TYPE'Unlifted
|
|
|
data Levity = Lifted | Unlifted
|
|
|
TYPE :: Levity -> *
|
|
|
type * = TYPE 'Lifted
|
|
|
type # = TYPE 'Unlifted
|
|
|
```
|
|
|
|
|
|
|
|
|
Instead, Proposal B2 suggests the following generalization:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataBoxity=Boxed|UnboxeddataLevity=Lifted|UnliftedTYPE::Boxity->Levity->*type*=TYPE'Boxed'Lifted-- TYPE 'Boxed 'Unlifted is the kind of boxed, unlifted types-- TYPE 'Unboxed 'Unlifted is the kind of unboxed, unlifted types-- TYPE 'Unboxed 'Lifted is utterly wrong, and prohibited from ever appearing in a desugared programtypeB_L=TYPE'Boxed'Lifted-- just for this wiki pagetypeB_UL=TYPE'Boxed'Unlifted-- just for this wiki pagetypeUB_UL=TYPE'Unboxed'Unlifted-- just for this wiki page
|
|
|
data Boxity = Boxed | Unboxed
|
|
|
data Levity = Lifted | Unlifted
|
|
|
TYPE :: Boxity -> Levity -> *
|
|
|
type * = TYPE 'Boxed 'Lifted
|
|
|
-- TYPE 'Boxed 'Unlifted is the kind of boxed, unlifted types
|
|
|
-- TYPE 'Unboxed 'Unlifted is the kind of unboxed, unlifted types
|
|
|
-- TYPE 'Unboxed 'Lifted is utterly wrong, and prohibited from ever appearing in a desugared program
|
|
|
|
|
|
type B_L = TYPE 'Boxed 'Lifted -- just for this wiki page
|
|
|
type B_UL = TYPE 'Boxed 'Unlifted -- just for this wiki page
|
|
|
type UB_UL = TYPE 'Unboxed 'Unlifted -- just for this wiki page
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -279,10 +400,13 @@ This treatment is a simple extension of levity polymorphism, and it serves the s |
|
|
**Definition:** A **valued kind** is a kind of types that have values. In released GHC, the valued kinds are `*`, `#`, and `Constraint`. Proposal B2 suggests adding `TYPE 'Boxed 'Unlifted` and `TYPE 'Unboxed 'Unlifted` to this set.
|
|
|
|
|
|
|
|
|
|
|
|
(**Extension:** Edward Kmett would recommend
|
|
|
|
|
|
|
|
|
```
|
|
|
dataConstraintiness=Constraint|NotConstraintTYPE::Boxity->Levity->Constraintiness->*
|
|
|
data Constraintiness = Constraint | NotConstraint
|
|
|
TYPE :: Boxity -> Levity -> Constraintiness -> *
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -294,18 +418,23 @@ to allow better inference around tuple types. While RAE thinks this would actual |
|
|
Proposal 1, above, allows users to make unlifted data types, separately from lifted ones. RAE is worried that this approach would lead to tons of duplication of data types (we might need **four** variants of `Maybe`, for example) and wants a more uniform way forward. Hence this Proposal B3.
|
|
|
|
|
|
|
|
|
|
|
|
The proposal will explain by way of example. (The use of GADT syntax here is incidental, but it makes the text in this proposal work out better. The normal traditional-syntax declaration would have identical behavior.)
|
|
|
|
|
|
|
|
|
```
|
|
|
dataMaybe a whereJust:: a ->Maybe a
|
|
|
Nothing::Maybe a
|
|
|
data Maybe a where
|
|
|
Just :: a -> Maybe a
|
|
|
Nothing :: Maybe a
|
|
|
```
|
|
|
|
|
|
|
|
|
All we know about the type variable `a` is that it is used as an argument to `->`. Functions can naturally have any valued kind as an argument. But it would be silly to allow `a :: TYPE 'Unboxed 'Unlifted`, as we'll have trouble generating code for that. Furthermore, we wish to treat **all** datatypes as levity polymorphic in their return kind (the heart of Proposal B3). So, we infer this kind for `Maybe`:
|
|
|
|
|
|
|
|
|
```
|
|
|
Maybe:: forall (v1 ::Levity)(v2 ::Levity).TYPE'Boxed v1 ->TYPE'Boxed v2
|
|
|
Maybe :: forall (v1 :: Levity) (v2 :: Levity).
|
|
|
TYPE 'Boxed v1 -> TYPE 'Boxed v2
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -317,20 +446,27 @@ To reiterate: the levity polymorphism here is just to simplify the life of the p |
|
|
### A recursive example
|
|
|
|
|
|
|
|
|
|
|
|
Let's look at a recursive datatype to see how this works out:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataList a whereNil::List a
|
|
|
Cons:: a ->List a ->List a
|
|
|
data List a where
|
|
|
Nil :: List a
|
|
|
Cons :: a -> List a -> List a
|
|
|
```
|
|
|
|
|
|
|
|
|
After inference and with everything explicit, we would get
|
|
|
|
|
|
|
|
|
```
|
|
|
dataList:: forall (v1 ::Levity)(v2 ::Levity).TYPE'Boxed v1 ->TYPE'Boxed v2 whereNil:: forall (v1 ::Levity)(v2 ::Levity)(a ::TYPE'Boxed v1).List v1 v2 a
|
|
|
Cons:: forall (v1 ::Levity)(v2 ::Levity)(a ::TYPE'Boxed v1).
|
|
|
a ->List v1 v2 a ->List v1 v2 a
|
|
|
data List :: forall (v1 :: Levity) (v2 :: Levity).
|
|
|
TYPE 'Boxed v1 -> TYPE 'Boxed v2 where
|
|
|
Nil :: forall (v1 :: Levity) (v2 :: Levity) (a :: TYPE 'Boxed v1).
|
|
|
List v1 v2 a
|
|
|
Cons :: forall (v1 :: Levity) (v2 :: Levity) (a :: TYPE 'Boxed v1).
|
|
|
a -> List v1 v2 a -> List v1 v2 a
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -352,14 +488,20 @@ Of course, users are free to use levity polymorphic recursion to achieve other c |
|
|
## Proposal B4: Levity polymorphic functions
|
|
|
|
|
|
|
|
|
|
|
|
Carrying forward from Proposal B3, we could extend levity polymorphism to work on functions. For example, `map` could be inferred to have this type
|
|
|
|
|
|
|
|
|
```
|
|
|
map:: forall (v1 ::Levity)(v2 ::Levity)(v3 ::Levity)(v4 ::Levity)(a ::TYPE'Boxed v1)(b ::TYPE'Boxed v2).(a -> b)->[]@v1 @v3 a ->[]@v2 @v4 b
|
|
|
map :: forall (v1 :: Levity) (v2 :: Levity) (v3 :: Levity) (v4 :: Levity)
|
|
|
(a :: TYPE 'Boxed v1) (b :: TYPE 'Boxed v2).
|
|
|
(a -> b) -> [] @v1 @v3 a -> [] @v2 @v4 b
|
|
|
```
|
|
|
|
|
|
|
|
|
Here, `v1` and `v2` are the levities of `a` and `b`, respectively, and `v3` and `v4` are the levities of the argument and result lists, respectively. As previously articulated, we can't have proper levity polymorphic functions, instead requiring specialization. This would mean **sixteen**`map`s. That's quite a high number. But I (Richard) think all of the variants make sense. I'd love for there to be some optimization to prevent the need to export 16 definitions here, but I don't see one. In any case, I do think this would work swimmingly for users. Is it worth the cost? That's up for debate.
|
|
|
Here, `v1` and `v2` are the levities of `a` and `b`, respectively, and `v3` and `v4` are the levities of the argument and result lists, respectively. As previously articulated, we can't have proper levity polymorphic functions, instead requiring specialization. This would mean **sixteen** `map`s. That's quite a high number. But I (Richard) think all of the variants make sense. I'd love for there to be some optimization to prevent the need to export 16 definitions here, but I don't see one. In any case, I do think this would work swimmingly for users. Is it worth the cost? That's up for debate.
|
|
|
|
|
|
|
|
|
|
|
|
**Conjecture:** If we take this idea to its logical extreme -- of making all functions levity polymorphic in all of the datatypes mentioned -- then RAE believes that using `!` to control kinds in datatype definitions would not break any code.
|
|
|
|
... | ... | @@ -373,31 +515,44 @@ Here, `v1` and `v2` are the levities of `a` and `b`, respectively, and `v3` and |
|
|
Some of the examples given in the alternate proposals (B3 and B4) are not parametric polymorphism, but rather ad-hoc polymorphism of levities. For instance, the `map` example does not have one uniform implementation, but many based on the instantiations, and each case has quite different behavior.
|
|
|
|
|
|
|
|
|
|
|
|
However, there are many examples of functions that can be properly levity polymorphic, because they are just (at a low level) moving pointers around, and the levity only tracks the overall calling convention for those pointers, rather than the operation of the body of the function. The most immediate example is constructors of data types. If we have:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataT:: forall (l ::Levity).(a ::TYPE'Boxed l)->TYPE'Boxed'LiftedwhereC:: forall (l ::Levity)(a ::Type'Boxed l). a ->T a
|
|
|
data T :: forall (l :: Levity). (a :: TYPE 'Boxed l) -> TYPE 'Boxed 'Lifted where
|
|
|
C :: forall (l :: Levity) (a :: Type 'Boxed l). a -> T a
|
|
|
```
|
|
|
|
|
|
|
|
|
Then `C` is genuinely parametric in `l`. It accepts a pointer to a value that is either lifted or not, stores it, and matching on it later yields a pointer to a value with the same status. It is unclear to the present author whether `C` would also be genuinely parametric if `T` were parameterized on its levity status as well.
|
|
|
|
|
|
|
|
|
|
|
|
There are examples beyond constructors, though. All mutable cells for boxed types have the same behavior of simply storing a pointer, so put and get operations should be genuinely parametric. They simply preserve the calling conventions of things they are fed and return. Further, this area is quite rich, and enabling these parametric uses fixes problems with duplication, type safety and efficiency in primops. Right now one must choose between:
|
|
|
|
|
|
|
|
|
```
|
|
|
ArrayArray#-- not type safeArray#(Array a)-- has extra indirection
|
|
|
ArrayArray# -- not type safe
|
|
|
Array# (Array a) -- has extra indirection
|
|
|
```
|
|
|
|
|
|
|
|
|
whereas with levity polymorphic `Array#`, one could have `Array# (Array# a)` which is the best of both worlds (eliminating the need for duplication).
|
|
|
|
|
|
|
|
|
|
|
|
As a final thought, let's consider the `map` example:
|
|
|
|
|
|
|
|
|
```
|
|
|
map:: forall (v1 v2 v3 v4 ::Levity)(a ::TYPE'Boxed v1)(b ::TYPE'Boxed v2)(a -> b)->[]@v1 @v3 a ->[]@v2 @v4 b
|
|
|
map f []=[]map f (x:xs)=let y = f x
|
|
|
map :: forall (v1 v2 v3 v4 :: Levity)
|
|
|
(a :: TYPE 'Boxed v1)
|
|
|
(b :: TYPE 'Boxed v2)
|
|
|
(a -> b) -> [] @v1 @v3 a -> [] @v2 @v4 b
|
|
|
map f [] = []
|
|
|
map f (x:xs) =
|
|
|
let y = f x
|
|
|
ys = map f xs
|
|
|
in y:ys
|
|
|
```
|
... | ... | @@ -438,8 +593,9 @@ In fact, this minimal addition bears a strong resemblance to the original |
|
|
version of this proposal. However, it was noted that there is a problem with
|
|
|
the current meanting of `!a` in constructors. Given the declaration:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataT=C!Nat!Nat
|
|
|
data T = C !Nat !Nat
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -459,8 +615,10 @@ witness of this is simply an identity function that has an effect of forgetting |
|
|
that its argument must already be evaluated, because the values of type `!a` are
|
|
|
also valid values of type `a`. Then, if the match:
|
|
|
|
|
|
|
|
|
```
|
|
|
case t ofC x y ->...
|
|
|
case t of
|
|
|
C x y -> ...
|
|
|
```
|
|
|
|
|
|
|
... | ... | |