boring (empty) → 0

raw patch · 5 files changed

+286/−0 lines, 5 filesdep +adjunctionsdep +basedep +semigroupssetup-changed

Dependencies added: adjunctions, base, semigroups, tagged, transformers, void

Files

ChangeLog.md +4/−0
LICENSE +30/−0
Setup.hs +2/−0
boring.cabal +55/−0
src/Data/Boring.hs +195/−0

+ ChangeLog.md view

@@ -0,0 +1,4 @@+# Revision history for boring+## 0++- First version. Released on an unsuspecting world.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2017, Oleg Grenrus++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 Oleg Grenrus 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.

+ Setup.hs view

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

+ boring.cabal view

@@ -0,0 +1,55 @@+name:                boring+version:             0+synopsis:            Boring and Absurd types+description:+  * @Boring@ types are isomorphic to @()@.+  . +  * @Absurd@ types are isomorphic to @Void@.+  .+  See [What does () mean in Haskell -answer by Conor McBride](https://stackoverflow.com/questions/33112439/what-does-mean-in-haskell/33115522#33115522)+homepage:            https://github.com/phadej/boring+bug-reports:         https://github.com/phadej/boring/issues+license:             BSD3+license-file:        LICENSE+author:              Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>+copyright:           (c) 2017 Oleg Grenrus+category:            Data+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10+tested-with:+  GHC==7.4.2,+  GHC==7.6.3,+  GHC==7.8.4,+  GHC==7.10.3,+  GHC==8.0.2,+  GHC==8.2.1++source-repository head+  type:      git+  location:  https://github.com/phadej/boring.git++library+  exposed-modules:+    Data.Boring+  build-depends:+    base         >=4.5   && <4.11,+    adjunctions  >=4.3   && <4.4,+    tagged       >=0.8.5 && <0.9,+    transformers >=0.3   && <0.6++  if !impl(ghc >= 8.0)+    build-depends:+      semigroups         >=0.18.3   && <0.19+  if !impl(ghc >= 7.10)+    build-depends:+      void               >=0.7.2    && <0.8++  other-extensions:+    CPP+    FlexibleContexts+    GADTs+    TypeOperators+  hs-source-dirs:      src+  default-language:    Haskell2010

+ src/Data/Boring.hs view

@@ -0,0 +1,195 @@+{-# LANGUAGE CPP              #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE TypeOperators    #-}+-- | 'Boring' and 'Absurd' classes. One approach.+--+-- Different approach would be to have+--+-- @+-- -- none-one-tons semiring+-- data NOT = None | One | Tons+--+-- type family Cardinality (a :: *) :: NOT+--+-- class Cardinality a ~ None => Absurd a where ...+-- class Cardinality a ~ One  => Boring a where ...+-- @+--+-- This would make possible to define more instances, e.g.+--+-- @+-- instance (Mult (Cardinality a) (Cardinality b) ~ None) => Absurd (a, b) where ...+-- @+--+-- === Functions+--+-- Function is an exponential:+--+-- @+-- Cardinality (a -> b) ~ Exponent (Cardinality b) (Cardinality a)+-- @+--+-- or shortly @|a -> b| = |b| ^ |a|@. This gives us possible instances:+--+-- * @|a| = 0 => |a -> b| = m ^ 0 = 1@, i.e. @'Absurd' a => 'Boring' (a -> b)@, or+--+-- * @|b| = 1 => |a -> b| = 1 ^ n = 1@, i.e. @'Boring' b => 'Boring' (a -> b)@.+--+-- Both instances are 'Boring', but we chose to define the latter.+--+-- === Note about adding instances+--+-- At this moment this module misses a lot of instances,+-- please make a patch to add more. Especially, if the package is already+-- in the transitive dependency closure.+--+-- E.g. any possibly empty container @f@ has @'Absurd' a => 'Boring' (f a)@+--+module Data.Boring (+    -- * Classes+    Boring (..),+    Absurd (..),+    -- * More integeresting stuff+    vacuous,+    boringRep,+    untainted,+    ) where++import Control.Applicative   (Const (..))+import Data.Functor.Identity (Identity (..))+import Data.Functor.Rep      (Representable (..))+import Data.List.NonEmpty    (NonEmpty (..))+import Data.Proxy            (Proxy (..))+import Data.Tagged           (Tagged (..))++import qualified Data.Void as V++#if MIN_VERSION_base(4,7,0)+import qualified Data.Type.Equality as Eq+#endif++-------------------------------------------------------------------------------+-- Boring+-------------------------------------------------------------------------------++-- | 'Boring' types which contains one thing, also+-- 'boring'. There is nothing interesting to be gained by+-- comparing one element of the boring type with another,+-- because there is nothing to learn about an element of the+-- boring type by giving it any of your attention.+--+-- /Boring Law:/+--+-- @+-- 'boring' == x+-- @+--+-- /Note:/ This is different class from @Default@.+-- @Default@ gives you /some/ value,+-- @Boring@ gives you an unique value.+--+-- Also note, that we cannot have instances for e.g.+-- 'Either', as both+-- @('Boring' a, 'Absurd' b) => Either a b@ and+-- @('Absurd' a, 'Boring' b) => Either a b@ would be valid instances.+--+-- Another useful trick, is that you can rewrite computations with +-- 'Boring' results, for example @foo :: Int -> ()@, __if__ you are sure+-- that @foo@ is __total__.+--+-- > {-# RULES "less expensive" foo = boring #-}+--+-- That's particularly useful with equality ':~:' proofs.+--+class Boring a where+    boring :: a++instance Boring () where+    boring = ()++instance Boring b => Boring (a -> b) where+    boring = const boring++instance Boring (Proxy a) where+    boring = Proxy++instance Boring a => Boring (Const a b) where+    boring = Const boring++instance  Boring b => Boring (Tagged a b) where+    boring = Tagged boring++instance Boring a => Boring (Identity a) where+    boring = Identity boring++instance (Boring a, Boring b) => Boring (a, b) where+    boring = (boring, boring)++instance (Boring a, Boring b, Boring c) => Boring (a, b, c) where+    boring = (boring, boring, boring)++instance (Boring a, Boring b, Boring c, Boring d) => Boring (a, b, c, d) where+    boring = (boring, boring, boring, boring)++instance (Boring a, Boring b, Boring c, Boring d, Boring e) => Boring (a, b, c, d, e) where+    boring = (boring, boring, boring, boring, boring)++-- | Recall regular expressions, kleene star of empty regexp is epsilon!+instance Absurd a => Boring [a] where+    boring = []++-- | @'Maybe' a = a + 1@, @0 + 1 = 1@.+instance Absurd a => Boring (Maybe a) where+    boring = Nothing++#if MIN_VERSION_base(4,7,0)+-- | Type equality is 'Boring' too.+instance a ~ b => Boring (a Eq.:~: b) where+    boring = Eq.Refl+#endif++-------------------------------------------------------------------------------+-- Absurd+-------------------------------------------------------------------------------++-- | The 'Absurd' type is very exciting, because if somebody ever gives you a+-- value belonging to it, you know that you are already dead and in Heaven and+-- that anything you want is yours.+--+-- Similarly as there are many 'Boring' sums, there are many 'Absurd' products,+-- so we don't have 'Absurd' instances for tuples.+class Absurd a where+    absurd :: a -> b++instance Absurd V.Void where+    absurd = V.absurd++instance (Absurd a, Absurd b) => Absurd (Either a b) where+    absurd (Left a) = absurd a+    absurd (Right b) = absurd b++instance Absurd a => Absurd (NonEmpty a) where+    absurd (x :| _) = absurd x++instance Absurd a => Absurd (Identity a) where+    absurd = absurd . runIdentity++-------------------------------------------------------------------------------+-- More interesting stuff+-------------------------------------------------------------------------------++-- | If 'Absurd' is uninhabited then any 'Functor' that holds only+-- values of type 'Absurd' is holding no values.+vacuous :: (Functor f, Absurd a) => f a -> f b+vacuous = fmap absurd++-- | If an index of 'Representable' @f@ is 'Absurd', @f a@ is 'Boring'.+boringRep :: (Representable f, Absurd (Rep f)) => f a+boringRep = tabulate absurd++-- | If an index of 'Representable' @f@ is 'Boring', @f@ is isomorphic to 'Identity'.+--+-- See also @Settable@ class in @lens@.+untainted :: (Representable f, Boring (Rep f)) => f a -> a+untainted = flip index boring