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.

Atravers 11:46, 12 February 2020 (UTC)