diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,1 @@
+# Changelog for `singletons-default`
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+# singletons-default
+ dependently typed optional values with defaults
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/singletons-default.cabal b/singletons-default.cabal
new file mode 100644
--- /dev/null
+++ b/singletons-default.cabal
@@ -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
diff --git a/src/Data/Default/Singletons.hs b/src/Data/Default/Singletons.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Default/Singletons.hs
@@ -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