4 ms·

I never heard of Uniqueness type (https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type). Anyone can simply explain pro/co

• tempodox 5y ago
  The IO monad (in Haskell) will always be the same, no matter how much I/O you perform. A unique File type, for instance, will be different before and after I/O, reflecting that side effects are not idempotent. In other words, a change in mutable state is reflected in a change of type.
  • cies 5y ago
    I'd love to see an example of this (the wikipedia page is not very clear to me). Is there a Clean or Idris program somewhere I can have a look at?
    • cjfd 5y ago
      I studied clean a very long time ago, maybe 20 years, so I have no idea any more what the code looks like, but I can attempt to tell you the basic idea of this. There are objects that you cannot copy and also not use in multiple places as a function argument. E.g., if something is a file it is subject to these restrictions and functions that write to the file would accept the file as an argument and return a new object of type file that stands for the modified version of the file. This forces an explicit sequencing of side effects. This prevents the old version of the file still being usable in the code.
    • toolslive 5y ago
      Mercury has them too: https://www.mercurylang.org/information/doc-latest/mercury_ref/Unique-modes.html https://www.mercurylang.org/information/doc-latest/mercury_r... useful for things like file descriptors. The type system will, for example prevent sharing of your file descriptors between threads.
      • deleted 5y ago
        [deleted]
      • dejj 5y ago
        I consider Unique as user-defined affine types— half of what makes up a linear type. Clean and Mercury are both mentioned in: https://en.m.wikipedia.org/wiki/Substructural_type_system https://en.m.wikipedia.org/wiki/Substructural_type_system