singletons-default (empty) → 0.1.0.0

raw patch · 6 files changed

+441/−0 lines, 6 filesdep +basedep +data-defaultdep +singletonssetup-changed

Dependencies added: base, data-default, singletons, singletons-base

Files

CHANGELOG.md +1/−0
LICENSE +21/−0
README.md +2/−0
Setup.hs +2/−0
singletons-default.cabal +43/−0
src/Data/Default/Singletons.hs +372/−0

+ CHANGELOG.md view

@@ -0,0 +1,1 @@+# Changelog for `singletons-default`

+ LICENSE view

@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2024 Eitan Chatav++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

+ README.md view

@@ -0,0 +1,2 @@+# singletons-default+ dependently typed optional values with defaults

+ Setup.hs view

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

+ singletons-default.cabal view

@@ -0,0 +1,43 @@+cabal-version: 2.2++-- This file has been generated from package.yaml by hpack version 0.36.0.+--+-- see: https://github.com/sol/hpack++name:           singletons-default+version:        0.1.0.0+synopsis:       An optional type with type level default+description:    Please see the README on GitHub at <https://github.com/morphismtech/singletons-default#readme>+category:       Data+homepage:       https://github.com/morphismtech/singletons-default#readme+bug-reports:    https://github.com/morphismtech/singletons-default/issues+author:         Eitan Chatav+maintainer:     eitan.chatav@gmail.com+copyright:      2024 Eitan Chatav+license:        BSD-3-Clause+license-file:   LICENSE+build-type:     Simple+extra-doc-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/morphismtech/singletons-default++library+  exposed-modules:+      Data.Default.Singletons+  other-modules:+      Paths_singletons_default+  autogen-modules:+      Paths_singletons_default+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base >=4.7 && <5+    , data-default >=0.7.1 && <0.8+    , singletons >=3.0.2 && <3.1+    , singletons-base >=3.1.1 && <3.5+  default-language: Haskell2010

+ src/Data/Default/Singletons.hs view

@@ -0,0 +1,372 @@+{-|+Module      : Data.Default.Singletons+Description : Provides singleton-based default values and optional types.+Copyright   : (c) 2024, Eitan Chatav+License     : MIT+Maintainer  : eitan.chatav@gmail.com+Stability   : experimental+Portability : non-portable (GHC extensions)++This module defines an `Opt`ional type with+either a `Def`ault promoted value,+or `Some` specific demoted value.++>>> definite (Def :: Opt True)+True+>>> definite (Some False :: Opt True)+False+>>> definite (Some True :: Opt True)+True+>>> maybe "def" show (perhaps (Def :: Opt True))+"def"+>>> maybe "def" show (perhaps (Some True :: Opt True))+"True"+>>> maybe "def" show (perhaps (Some False :: Opt True))+"False"++Promoted datakinds and their `Demote`d datatypes include:++>>> :kind! Demote Symbol+Demote Symbol :: *+= Text+>>> :kind! Demote Natural+Demote Natural :: *+= Natural+>>> :kind! Demote Char+Demote Char :: *+= Char+>>> :kind! Demote Bool+Demote Bool :: *+= Bool+>>> :kind! Demote [k]+Demote [k] :: *+= [Demote k]+>>> :kind! Demote String+Demote String :: *+= [Char]+>>> :kind! Demote (Either k j)+Demote (Either k j) :: *+= Either (Demote k) (Demote j)+>>> :kind! Demote (k,j)+Demote (k,j) :: *+= (Demote k, Demote j)++Because there is no promoted `Integer` and `Rational` datakinds,+this module defines them as `Z` and `Q`.++>>> :kind! Demote Z+Demote Z :: *+= Integer+>>> :kind! Demote Q+Demote Q :: *+= Ratio Integer++The `Opt` type comes with+`Num`, `Integral`, `Fractional`, and `Real` instances,+using `definite` values to do arithmetic;+and `IsString` and `IsList` instances,+which let you use literals to construct `Opt`.++>>> "text" :: Opt ("hello" :: Symbol)+Some "text"+>>> "string" :: Opt (['a','b','c'] :: String)+Some "string"+>>> [1, 2] :: Opt ('[] :: [Natural])+Some [1,2]+>>> Def + 0 :: Opt (Pos 1 :: Z)+Some 1+>>> 0.5 + Def :: Opt (Neg 1 :% 3 :: Q)+Some (1 % 6)++-}++{-# LANGUAGE+ConstraintKinds+, DataKinds+, FlexibleContexts+, FlexibleInstances+, GADTs+, LambdaCase+, PolyKinds+, RankNTypes+, ScopedTypeVariables+, StandaloneDeriving+, TypeApplications+, TypeFamilies+, TypeOperators+, UndecidableInstances+#-}++module Data.Default.Singletons+  ( -- | Optional Datatype+    Opt (..)+  , SingDef+  , optionally+  , definite+  , perhaps+  , demote+    -- | Promoted Datakinds+  , Z (..)+  , Neg+  , Q (..)+  , SInteger (..)+  , SRational (..)+  ) where++import Control.Applicative+import Data.Default+import GHC.IsList+import Data.Ratio+import GHC.TypeNats+import Data.Singletons+import Data.String+import Prelude.Singletons ()++{- |+`Opt`ional type with+either a `Def`ault promoted value @def@,+or `Some` specific `Demote`d value.++`Opt` is a `Monoid` which yields the leftmost `Some`.++>>> mempty :: Opt "xyz"+Def+>>> Def <> "abc" <> "qrs" :: Opt "xyz"+Some "abc"++You can use `Opt` as an optional function argument.++>>> let greet (name :: Opt "Anon") = "Welcome, " <> definite name <> "."+>>> greet "Sarah"+"Welcome, Sarah."+>>> greet Def+"Welcome, Anon."++Or, you can use `Opt` as an optional field in your record type.++>>> :{+data Person = Person+  { name :: Text+  , age :: Natural+  , alive :: Opt (True :: Bool)+  }+:}+>>> let isAlive person = definite (alive person)+>>> let jim = Person {name = "Jim", age = 40, alive = Def}+>>> isAlive jim+True++-}+data Opt (def :: k) where+  Def :: SingDef def => Opt (def :: k)+  Some :: SingDef def => Demote k -> Opt (def :: k)++{- | Constraint required to `demote` @@def@. -}+type SingDef (def :: k) = (SingI def, SingKind k)++instance Semigroup (Opt (def :: k)) where+  Def <> opt = opt+  Some x <> _ = Some x++instance SingDef def => Monoid (Opt def) where+  mempty = Def++deriving instance (SingDef def, Show (Demote k))+  => Show (Opt (def :: k))++deriving instance (SingDef def, Read (Demote k))+  => Read (Opt (def :: k))++deriving instance (SingDef def, Eq (Demote k))+  => Eq (Opt (def :: k))++deriving instance (SingDef def, Ord (Demote k))+  => Ord (Opt (def :: k))++instance SingDef def+  => Default (Opt (def :: k)) where def = Def++instance (SingDef def, Num (Demote k))+  => Num (Opt (def :: k)) where+    x + y = Some $ definite x + definite y+    x * y = Some $ definite x * definite y+    abs x = Some $ abs (definite x)+    signum x = Some $ signum (definite x)+    fromInteger x = Some $ fromInteger x+    negate x = Some $ negate (definite x)+    x - y = Some $ definite x - definite y++instance (SingDef def, Fractional (Demote k))+  => Fractional (Opt (def :: k)) where+    recip x = Some $ recip (definite x)+    x / y = Some $ definite x / definite y+    fromRational x = Some $ fromRational x++instance (SingDef def, IsString (Demote k))+  => IsString (Opt (def :: k)) where+    fromString x = Some $ fromString x++instance (SingDef def, IsList (Demote k))+  => IsList (Opt (def :: k)) where+    type Item (Opt (def :: k)) = Item (Demote k)+    fromList xs = Some $ fromList xs+    fromListN n xs = Some $ fromListN n xs+    toList x = toList $ definite x++{- |+Constructs an `Opt` from a `Maybe`.+`Nothing` maps to `Def`,+and `Just` maps to `Some`.+-}+optionally :: SingDef def => Maybe (Demote k) -> Opt (def :: k)+optionally = maybe Def Some++{- |+Deconstructs an `Opt` to a `Demote`d value.+`Def` maps to `demote` @@def@,+and `Some` maps to its argument.+-}+definite :: forall k def. Opt (def :: k) -> Demote k+definite = \case+  Def -> demote @def+  Some a -> a++{- |+Deconstructs an `Opt` to an `Alternative` `Demote`d value.+`Def` maps to `empty`,+and `Some` maps to `pure`,+inverting `optionally`.+-}+perhaps :: Alternative m => Opt (def :: k) -> m (Demote k)+perhaps = \case+  Def -> empty+  Some a -> pure a++{- |+Datakind `Z`, promoting `Integer`,++>>> :kind! Demote Z+Demote Z :: *+= Integer++with `Pos` for constructing nonnegative integer types,+and `Neg` for constructing nonpositive integer types.++>>> demote @(Pos 90210)+90210+>>> demote @(Neg 5)+-5+>>> demote @(Neg 0)+0+>>> demote @(Pos 0)+0++-}+data Z = Pos Natural | NegOneMinus Natural+  deriving (Eq, Ord, Read, Show)++{- | Type family for negating a `Natural`.-}+type family Neg n where+  Neg 0 = Pos 0+  Neg n = NegOneMinus (n - 1)++instance Real Z where+  toRational = toRational . toInteger++instance Integral Z where+  toInteger (Pos n) = toInteger n+  toInteger (NegOneMinus n) = negate 1 - toInteger n+  quotRem x y =+    let (q,r) = quotRem (toInteger x) (toInteger y)+    in (fromInteger q, fromInteger r)+  divMod x y =+    let (q,r) = divMod (toInteger x) (toInteger y)+    in (fromInteger q, fromInteger r)++instance Enum Z where+  toEnum = fromIntegral+  fromEnum = fromIntegral++instance Num Z where+  x + y = fromInteger (toInteger x + toInteger y)+  x * y = fromInteger (toInteger x * toInteger y)+  abs x = fromInteger (abs (toInteger x))+  signum x = fromInteger (signum (toInteger x))+  negate x = fromInteger (negate (toInteger x))+  x - y = fromInteger (toInteger x - toInteger y)+  fromInteger x =+    if signum x >= 0+    then Pos (fromInteger x)+    else NegOneMinus (fromInteger (negate (1 + x)))++{- | Singleton representation for the `Z` kind. -}+data SInteger (n :: Z) where+  SPos :: SNat n -> SInteger (Pos n)+  SNegOneMinus :: SNat n -> SInteger (NegOneMinus n)++type instance Sing = SInteger++instance SingKind Z where+  type Demote Z = Integer+  fromSing = \case+    SPos n -> fromIntegral (fromSing n)+    SNegOneMinus n -> negate 1 - fromIntegral (fromSing n)+  toSing n = withSomeSing n SomeSing++instance KnownNat n => SingI (Pos n) where+  sing = SPos sing++instance KnownNat n => SingI (NegOneMinus n) where+  sing = SNegOneMinus sing++{- |+Datakind `Q`, promoting `Rational`,++>>> :kind! Demote Q+Demote Q :: *+= Ratio Integer++with `:%` for constructing rational types.++>>> demote @(Pos 7 :% 11)+7 % 11+>>> demote @(Neg 4 :% 2)+(-2) % 1++-}+data Q = (:%) Z Natural+  deriving (Eq, Ord, Show, Read)++instance Real Q where+  toRational (x :% y) = fromRational (toInteger x % toInteger y)++instance Fractional Q where+  recip (Pos x :% y) = (Pos y :% x)+  recip (NegOneMinus x :% y) = (NegOneMinus (y - 1) :% (1 + x))+  fromRational x = (fromInteger (numerator x) :% fromInteger (denominator x))++instance Num Q where+  x + y = fromRational (toRational x + toRational y)+  x * y = fromRational (toRational x * toRational y)+  abs x = fromRational (abs (toRational x))+  signum x = fromRational (signum (toRational x))+  negate x = fromRational (negate (toRational x))+  x - y = fromRational (toRational x - toRational y)+  fromInteger x = fromRational (fromInteger x)++{- | Singleton representation for the `Q` kind. -}+data SRational (n :: Q) where+  SRational :: SInteger n -> SNat m -> SRational (n :% m)++type instance Sing = SRational++instance SingKind Q where+  type Demote Q = Rational+  fromSing (SRational num denom)+    = fromRational+    $ toRational (fromSing num)+    / toRational (fromSing denom)+  toSing q = withSomeSing q SomeSing++instance (SingI num, SingI denom) => SingI (num :% denom) where+  sing = SRational sing sing