Uniqueness annotations for types
Since Haskell 1.3, strictness annotations have been available for use with type declarations:
data Complex a = !a :+ !a
Usually, this is all that's required - rarely is there a subsequent need to annotate the types (fixed or variable) in other Haskell entities.
Could a similar annotation be made available for uniqueness? Let's borrow a small piece of Clean syntax:
newtype UUID = MkUUID *Integer
data Label a = MkLabel *a
Similar to those for strictness, uniqueness annotations would largely be administered by the Haskell implementation - the obvious difference being the implementation's reaction to values of annotated types being reused e.g:
ghci> :t \l@(MkLabel x) -> (l, MkLabel x)
<interactive>:1:1: error:
Attempt to reuse value deemed unique: x :: a
by type declaration: data Label a = MkLabel *a
in structured value: (l, MkLabel x) :: (Label a, Label a)
ghci> :t \i@(MkUUID _) -> (i, i)
<interactive>:3:1: error:
Attempt to reuse value implied unique: i :: UUID
by type declaration: newtype UUID = MkUUID *Integer
in structured value: (i, i) :: (UUID, UUID)
ghci> :t \(MkLabel x) -> repeat x
<interactive>:1:1: error:
Attempt to reuse value deemed unique: x :: a
by type declaration: data Label a = MkLabel *a
in application: repeat x :: [a]
ghci> :t (\i -> let f = const i in (f 0, f 1)) (undefined :: UUID)
<interactive>:3:1: error:
Attempt to reuse value implied unique: i :: UUID
by type declaration: newtype UUID = MkUUID *Integer
with local binding: f = const i
in structured value: (f 0, f 1) :: (UUID, UUID)
ghci> :t \(MkLabel x) -> x
\(MkLabel x) -> x :: Label a -> a
ghci> :t \i -> (i+1, MkUUID i)
\i -> (i+1, MkUUID i) :: Integer -> (Integer, UUID)
ghci>
The expectation here is that a simple annotation instead of an intricate extension would minimise the need to manually propagate uniqueness throughout the sources for existing and future Haskell programs and libraries.
What about linear types?
Linear types would be just a specific use of uniqueness annotations (and a little syntactic sugar), with an implementation expanding the type a ⊸ b
to *a -> b
.
See also:
Atravers 11:46, 12 February 2021 (UTC)