Dependent types using singleton types

{-# language DataKinds, PolyKinds, ScopedTypeVariables, UndecidableInstances,
    FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies, RankNTypes,
    LambdaCase, TypeOperators, ConstraintKinds #-}

import GHC.TypeLits
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Decide
import Data.Constraint

-- Witnesses
--------------------------------------------------------------------------------
-- for https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html
{-

Generally, the best practice is to avoid the functions
and exports from GHC.TypeLits and instead use the *singletons*
infrastructure because the native TypeLits operations don't
interoperate with singletons by default.

So:
  - Don't use KnownNat or KnownSymbol,
    and don't use the ugly "(KnownNat n) => Proxy n -> t" idiom
  - An explicit parameter is "Sing x"
  - An implicit parameter is "SingI x"
  - Convert from explicit to implicit with "singInstance" or "withSingI"
  - Convert from implicit to explicit with "sing"

The conversion from explicit to implicit essentially works the same way
as in Edward Kmett's Data.Reflection library.

The upshot here is that once we have singleton functions, we automatically
have all the explicit witnesses for function results, and we also get
all the implicit witnesses by the general "explicit->implicit" conversion.

-}

-- TypeNat witnesses

-- explicit witnesses are given by singleton functions

n1 = sing :: Sing 2
n2 = sing :: Sing 3

n3 = n1 %:+ n2 -- addition
n4 = n1 %:* n2 -- multiplication

n3' :: Integer
n3' = fromSing n3 -- 5

n4' :: Integer
n4' = fromSing n4 -- 6

-- implicit witnesses

-- Note the funky Num class on the kind level
-- Also, we only use "Dict" here for illustration purposes, in real code
-- we would just create the SingI instances on the fly, as needed.
implicitWitnessTest :: SNum (KindOf a) => Sing a -> Sing b -> Dict (SingI (a :+ b))
implicitWitnessTest a b = withSingI (a %:+ b) Dict

-- leave "a" implicit plus return the singletons analogue of Dict:
implicitWitnessTest2 ::
  forall a b. SingI (a :: Nat) => Sing b -> SingInstance (a :+ b)
implicitWitnessTest2 b = singInstance ((sing :: Sing a) %:+ b)

-- Also: convert a piece of demoted data to some singleton
-- This is a just a sometimes nicer version of "toSing"
withSomeSingtest :: IO ()
withSomeSingtest = do
  withSomeSing True (\case STrue -> print "got true"; SFalse -> print "got false")


{-
So, the witness generators are just singleton functions + conversion.

Note here that "Sing" is often a lot more convenient to use that "SingI".
That's because if we do any sort of computation on singleton values, we
need explicit parameters. Also, if there's any sort of ambiguity about
which parameters we pass to which functions, or about the order of
parameters, we need to specify it with type annotations, proxies or
explicit singletons, and explicit singletons are again the cleanest way.

95% of the time singleton arguments are operationally just like normal
arguments, so there's no reason to make them implicit. Similarly,
"withNatOp" is more straightforwardly expressed with explicit Sing
parameters. In short: most of the time use Sing instead of SingI or Proxy.

-}

-- List singletons & manipulation
--------------------------------------------------------------------------------

type KnownNats (xs :: [Nat]) = SingI xs
type NatList (xs :: [Nat]) = Sing xs
type SomeNats = SomeSing ('KProxy :: KProxy [Nat])

-- This one throws error on negative input, although not on conversion,
-- only on subsequent operations.
someNatsValPos :: [Integer] -> SomeNats
someNatsValPos = toSing

-- Since the safe conversion is missing from *singletons*, let's
-- implement it
safeIntegerSing :: Integer -> Maybe (SomeSing (KindOf 0))
safeIntegerSing =
  fmap (\(SomeNat (p :: Proxy n)) -> SomeSing (sing :: Sing n)) . someNatVal

sequenceSome :: [SomeSing ('KProxy :: KProxy k)] -> SomeSing ('KProxy :: KProxy [k])
sequenceSome = foldr (\(SomeSing x) (SomeSing xs) -> SomeSing (SCons x xs)) (SomeSing SNil)

someNatsVal :: [Integer] -> Maybe SomeNats
someNatsVal = fmap sequenceSome . traverse safeIntegerSing


-- Note : "KnownNats ns" is equivalent to "NatList ns", so it's redundant here
-- reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r
reifyNats :: [Integer] -> (forall ns. NatList ns -> r) -> r
reifyNats = withSomeSing

reifyNats' :: [Integer] -> r -> (forall ns. NatList ns -> r) -> r
reifyNats' ns r f = maybe r (\(SomeSing ns) -> f ns) (someNatsVal ns)

-- "Decision" is a bit more informative than "Maybe"
sameNats :: NatList ns -> NatList ms -> Decision (ns :~: ms)
sameNats = (%~)

-- We do the elimination generally.
listElim ::
     forall (p :: [a] -> *).
     p '[]
  -> (forall x xs. Sing (x ': xs) -> p xs -> p (x ': xs))
  -> forall (xs :: [a]). Sing xs -> p xs
listElim z f SNil         = z
listElim z f (SCons x xs) = f (SCons x xs) (listElim z f xs)

-- Actually, we can do even more generally if we switch to proper
-- type functions. Basically, this lets us fold with type families.
listElim' ::
     forall (p :: TyFun [a] * -> *).
     Proxy p
  -> p @@ '[]
  -> (forall x xs. Sing (x ': xs) -> p @@ xs -> p @@ (x ': xs))
  -> forall (xs :: [a]). Sing xs -> p @@ xs
listElim' p z f SNil         = z
listElim' p z f (SCons x xs) = f (SCons x xs) (listElim' p z f xs)



-- In general, SomeNat is equivalent to Integer,
-- SomeSymbol is equivalent to String, etc...
-- A demoted value carries the same amount of information as
-- a boxed-up singleton.

-- This is the reason why "traverseSList" below is more general
-- than your "traverseNatList" (even if we specialize on Nat)

-- "ak" is only introduced to reduce clutter. We use ~ as type-level "let" binding
traverseSList ::
     forall (xs :: [a]) f b ak.
     (ak ~ ('KProxy :: KProxy a), Applicative f, SingKind ak)
  => (DemoteRep ak -> f b)
  -> SList xs -> f [b]
traverseSList f = traverse f . fromSing

-- Closer to original type with more "SomeSing"
traverseSList' ::
     forall (xs :: [a]) f ak.
     (ak ~ ('KProxy :: KProxy a), Applicative f, SingKind ak)
  => (DemoteRep ak -> f (SomeSing ('KProxy :: KProxy b)))
  -> SList xs -> f (SomeSing ('KProxy :: KProxy [b]))
traverseSList' f = fmap sequenceSome . traverseSList f

-- The standard singleton map; this one preserves the most information
mapNatList ::
  Sing (f :: TyFun Nat b -> *) -> Sing (xs :: [Nat]) -> Sing (MapSym2 f xs)
mapNatList = sMap

mapNatList' :: (Integer -> Integer) -> Sing (xs :: [Nat]) -> [Integer]
mapNatList' f = map f . fromSing

mapNatList'' :: (Integer -> Integer) -> Sing (xs :: [Nat]) -> SomeNats
mapNatList'' f = toSing . map f . fromSing


-- The functions are the same for SymbolList etc, everything can be
-- generalized to cover the Symbol stuff too.
--------------------------------------------------------------------------------