Uniqueness annotations for types

From HaskellWiki

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?[edit]

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)