ann (empty) → 1.0.0

raw patch · 6 files changed

+326/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

• ChangeLog.md +5/−0
• LICENSE +30/−0
• README.md +35/−0
• Setup.hs +2/−0
• ann.cabal +35/−0
• src/Data/Ann.hs +219/−0

@@ -0,0 +1,5 @@+# Changelog for ann++## v1.0.0++- Initial release

@@ -0,0 +1,30 @@+Copyright Arnaud Spiwack (c) 2022++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Arnaud Spiwack nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,35 @@+# Ann++This package introduces a type `Ann a` to annotate data types with+information which doesn't influence the behaviour of your+program. These annotations can then be displayed, as assistance to the+user.++## Examples++### Variable names++You are writing a programing language, and representing binder as [de+Bruijn indices](https://en.wikipedia.org/wiki/+De_Bruijn_index). Nevertheless you want to keep the variable names+written by the user, to be able to interact with them on these terms+(_e.g._ in error messages). With 'Ann' it would look like this:++```haskell+data Term+  = Var Int+  | App Term Term+  | Lam (Ann String) Term+  deriving (Eq)+```++Thanks to the 'Ann' type, you can derive the intended equality: the+user's choice of variable doesn't change the term (this is called+α-equivalence).++### Validation monad++The [Validation](https://hackage.haskell.org/package/validation)+applicative can be made into a monad. Specifically `Validation (Ann+e)` is a monad, as I explained [in a Twitter+thread](https://twitter.com/aspiwack/status/1511987089562341377).

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,35 @@+cabal-version: 1.12++name:           ann+version:        1.0.0+synopsis:       Informative annotations which don't change equality+description:+    This package introduces a type @Ann a@ to annotate data types+    with information which doesn't influence the behaviour of your+    program. These annotations can then be displayed, as assistance to+    the user.+category:       Data+homepage:       https://github.com/aspiwack/haskell-ann#readme+bug-reports:    https://github.com/aspiwack/haskell-ann/issues+author:         Arnaud Spiwack+maintainer:     arnaud@spiwack.net+copyright:      2022 Arnaud Spiwack+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/aspiwack/haskell-ann++library+  exposed-modules:+      Data.Ann+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+  default-language: Haskell2010

@@ -0,0 +1,219 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE StandaloneDeriving #-}++-- | This module introduces a type @'Ann' a@ to annotate data types with+-- information which doesn't influence the behaviour of your program. These+-- annotations can then be displayed, as assistance to the user.+--+-- = Examples+--+-- == Variable names+--+-- You are writing a programing language, and representing binder as [de Bruijn+-- indices](https://en.wikipedia.org/wiki/De_Bruijn_index). Nevertheless you+-- want to keep the variable names written by the user, to be able to interact+-- with them on these terms (/e.g./ in error messages). With 'Ann' it would look+-- like this:+--+-- > data Term+-- >   = Var Int+-- >   | App Term Term+-- >   | Lam (Ann String) Term+-- >   deriving (Eq)+--+-- Thanks to the 'Ann' type, you can derive the intended equality: the user's+-- choice of variable doesn't change the term (this is called α-equivalence).+--+-- == Validation monad+--+-- The [Validation](https://hackage.haskell.org/package/validation) applicative+-- can be made into a monad. Specifically @Validation (Ann e)@ is a monad, as I+-- explained [in a Twitter+-- thread](https://twitter.com/aspiwack/status/1511987089562341377).+--+-- = __Theoretical considerations__+--+-- @'Ann' a@ is the+-- [quotient](https://en.wikipedia.org/wiki/Equivalence_class#quotient_set) of+-- @a@ by the total relation.+--+-- == What's so special about the total relation?+--+-- There are only two relations which can be defined generically on all sets:+-- the empty relation and the total relation (this can be proved by+-- parametricity). The quotient by the empty relation is 'Identity'. So the only+-- interesting generic quotient is 'Ann'.+--+-- Strictly speaking, sets are also equipped with the equality relation (and you+-- can derive the disequality relation from it). But quotienting by the equality+-- relation is the same as quotienting by the empty relation; and quotienting by+-- the disequality relation is the same as quotienting by the total relation.+--+-- Other quotients can be defined on individual sets using abstract types.+--+-- A consequence of defining 'Ann' generically on types is that it turns 'Ann'+-- into a functor. The functor structure is not particularly intersting. But+-- 'Ann' is also a monad.+--+-- > (>>=) :: Ann a -> (a -> Ann b) -> Ann b+--+-- That is: you are allowed to “look inside” an @'Ann' a@ only if you you are+-- producing an @'Ann' b@ to begin with. The program is not allowed to depend on+-- the choice of representative, yet @(>>=)@ gives the representative for us to+-- play with. But it's alright: it's only going to affect the representative in+-- @'Ann' b@, on which the program cannot depend either.+--+-- Something that I'd like to point out is that you really need the @a@ in the+-- @(a -> Ann b)@ argument. The reason is that 'Ann' is not isomorphic to @Const+-- ()@: @'Ann' b@ is isomorphic to @()@ if and only if @b@ is inhabited. @'Ann'+-- Void@, on the other hand, is isomorphic to @Void@. There is a sense in which+-- all that's interesting about 'Ann' stems from this fact.+--+-- The monadic @(>>=)@ is more or less explicitly in use in many dependently+-- typed theories (it is pretty hidden, but there in the typing rules for @Prop@+-- in Coq). For further reading see [Propositions as+-- [Types] ](https://ieeexplore.ieee.org/abstract/document/8133549) and+-- [Implicit and noncomputational arguments using+-- monads](https://hal.archives-ouvertes.fr/hal-00150900/).+--+-- === Algebras of 'Ann'+--+-- I haven't talked about @return@ yet+--+-- > 'return' :: a -> Ann a+--+-- It is the canonical projection to @'Ann' a@. It's exported as 'project' as+-- well.+--+-- This is really not relevant for the design or usage of the library, but it's+-- a natural question to ask: the algebras of 'Ann' (as a monad) are sets with+-- at most 1 element. Let @α :: Ann A -> A@ be such an algebra. Since @Ann A@+-- has at most one element, @α@ is constant. But, by the laws of algebra, we+-- also have @α ∘ return = id@, in particular @id :: A -> A@ is constant,+-- therefore @A@ has at most 1 element.+--+-- Conversely, if @A@ has at most 1 element, then @'Ann' A@ is isomorphic to+-- @A@, in particular @A@ is an algebra.+--+-- === Is there an equivalent for subsets?+--+-- Frankly at this point, this is just me rambling about stuff that I find+-- interesting. I'll get back to relevant stuff in the next section.+--+-- Subsets are the dual of quotients (in category-theory terms, quotients are+-- co-equalisers while subsets are equalisers). However, the category of set is+-- not its own dual, so that there is an interesting phenomenon for one doesn't+-- imply that there is to the other.+--+-- In the case at hand, there are two generically definable predicates as+-- well. The empty predicate and the full predicate. They both define boring+-- subset (the empty set, and the identity functor, respectively). So really,+-- 'Ann' is the only interesting case of the bunch.+--+-- == Extracting and IO+--+-- The type of 'extract' is+--+-- > extract :: Ann a -> IO a+--+-- There can't be a function `Ann a -> a` as this violates the quotient+-- condition (concretely that the program isn't affected by the choice of+-- representative of 'Ann a'). Well, more precisely, if such a function exists,+-- it must be constant. The existence of such a function is a form of choice (of+-- the axiom of choice fame). It's a very powerful principle, and probably not+-- desirable. I should give a citation here, but no source comes to mind at the+-- moment. You will have to trust me that in dependently typed language, this+-- is equivalent to choice (in particular it implies the excluded middle, if+-- 'Ann a' is used to represent propositions).+--+-- Ok, back to 'IO'. We don't want the choice of representative to affect the+-- semantics of the program, but we still want to print it out, so that the user+-- get their debug message or whatnot. 'IO' is our solution because it is+-- allowed to do non-deterministic actions in 'IO' (and printing usually+-- involves 'IO', so it doesn't cost much). So the semantics of extract is+-- “choose an arbitrary representative“; this representative need not be the+-- same each time. Of course we don't actually want an arbitrary representative+-- to be printed out: we want the one we put in. It would be difficult to give a+-- different implementation anyway. So we know, that, really, we will get the+-- representative we put in. But, strictly speaking, this is not, strictly+-- speaking, part of the semantics of the function (at least I don't know how to+-- make it so; it would be really nice to be able to).+--+-- This same trick is used in [Tackling the awkward+-- squad](https://simon.peytonjones.org/Tackling-the-awkward-squad/).+--+-- == Quotients and equivalence relations+--+-- This is even less related to the core of the package than the rest of this+-- section, but while we are on the subject of quotients, I'd like to address a+-- point.+--+-- You may have noticed that I repeatedly spoke of quotienting by “a relation”+-- throughout this document. If you are like me, though, you may have been+-- taught that a set is quotiented by an /equivalence relation/. It's because+-- equivalence classes form an equivalence relation. But it isn't essential to+-- the definition of quotient.+--+-- A quotient \(X/R\) of a set \(X\) is defined by its universal+-- property. Namely that a function \(f \in X/R \rightarrow C\)` is the same+-- thing as a function \(f' \in X \rightarrow C\) such that+-- \(x R y \Longrightarrow f x = f y\). That \(R\) is an equivalence relation doesn't+-- play a role in this definition. It turns out, however, that quotienting by+-- \(R\) or by its reflexive, symmetric and transitive closure yields the same+-- set.+++module Data.Ann+  ( Ann,+    project,+    extract,+    unsafeExtract,+  )+where++import Data.Functor.Identity++-- | @'Ann' a@ is the type of annotations of type @a@. It is such, in particular+-- that, for all @x :: 'Ann' a@ and @y :: 'Ann' a@, @x == y@.+newtype Ann a = Squash a+  deriving+    (Semigroup, Monoid, Read, Show)+    via (Identity a)++-- | See @Monad@ instance+deriving via Identity instance Functor Ann+-- | See @Monad@ instance+deriving via Identity instance Applicative Ann+-- | The particular choice of annotation may not affect the meaning of the+-- program. One way to prove to Haskell that you can safely depend on the+-- underlying annotation is to use it only to build an @'Ann' b@. The monad+-- instance gives you this ability. More (too much?) detail in the theoretical+-- considerations.+deriving via Identity instance Monad Ann++instance Eq (Ann a) where+  _ == _ = True++instance Ord (Ann a) where+  _ <= _ = True+  compare _ _ = EQ++-- | When all else fails – if neither the @Monad@ instance nor 'extract' fit+-- your need – you can use 'unsafeExtract' to observe the underlying value of an+-- annotation.+--+-- ⚠️ You /must/ prove that you are not using @'unsafeExtract ann@ in a way where+-- changing the value of @ann@ would change the behaviour of your program.+unsafeExtract :: Ann a -> a+unsafeExtract (Squash a) = a++-- | Extract the underlying value of an annotation. We have that @extract+-- . project = return@. But do keep in mind that valid refactoring can change+-- the underlying value of the annotation. As such, 'extract' is a+-- non-deterministic operation.+extract :: Ann a -> IO a+extract = return . unsafeExtract++-- | Create an annotation. See also 'extract'.+project :: a -> Ann a+project = Squash