View source for Uniqueness annotations for types

[[Category:Proposals]]
Since Haskell 1.3, ''strictness annotations'' have been available for use with type declarations:

<haskell>
data Complex a = !a :+ !a
</haskell>

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 [https://clean.cs.ru.nl/Clean Clean] syntax:

<haskell>
newtype UUID =  MkUUID *Integer

data Label a =  MkLabel *a
</haskell>

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:

<haskell>
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>
</haskell>

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''? ===

[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.31.5002&rep=rep1&type=pdf Linear types] would be just a specific use of uniqueness annotations (and a little syntactic sugar), with an implementation expanding the type <code>a ⊸ b</code> to <code>*a -> b</code>.

----
See also:

* [https://gitlab.haskell.org/ghc/ghc/-/issues/19799 GHC ticket 19799: Allow uniqueness annotations for types]



[[User:Atravers|Atravers]] 11:46, 12 February 2021 (UTC)