Difference between revisions of "Uniqueness annotations for types"

From HaskellWiki
Jump to navigation Jump to search
m (Wrong year >_<)
m (Link to related GHC ticket added)
 
Line 58: Line 58:
   
 
[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>.
 
[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]
  +
   
   

Latest revision as of 21:41, 16 August 2021

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)