Type Level ordered list in haskell

olist_working.hs

{-# language DataKinds #-}
{-# language PolyKinds #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language RankNTypes #-}
{-# language TypeFamilies #-}
{-# language TypeInType #-}
{-# language TypeFamilyDependencies #-}
{-# language UndecidableInstances #-}

module Main where

import Data.Type.Equality ((:~:)(..))
import qualified Data.Type.Equality as Equality
import Data.Kind (Type)

data Nat = Zero | Suc Nat

type family Sing = (r :: k -> Type) | r -> k

data SNat :: Nat -> Type where
  SZero :: SNat 'Zero
  SSuc  :: SNat n -> SNat ('Suc n)

data SBool :: Bool -> Type where
  STrue  :: SBool 'True
  SFalse :: SBool 'False

type instance Sing = SNat
type instance Sing = SBool

data GreaterThanEq :: Nat -> Nat -> Type where
  GreaterThanEqZero :: GreaterThanEq n 'Zero
  GreaterThanEqSuc :: GreaterThanEq n m -> GreaterThanEq ('Suc n) ('Suc m)

data Equivalence :: (x -> x -> Type) -> Type where
  Equivalence :: { equivalenceRefl  :: f a a
                 , equivalenceSym   :: f a b -> f b a
                 , equivalenceTrans :: f a b -> f b c -> f a c
                 } -> Equivalence f

data TotalOrder :: (x -> x -> Type) -> (x -> x -> Type) -> Type where
  TotalOrder ::
    { totalOrderAntisym :: forall a b. g a b -> g b a -> f a b
    , totalOrderTrans :: forall a b c. Sing a -> Sing b -> Sing c
                      -> GreaterThanEq a b -> GreaterThanEq b c -> GreaterThanEq a c
    , totalOrderTotal :: forall a b. Sing a -> Sing b -> Either (g b a) (g a b)
    , totalOrderReflexive :: forall a b. Sing a -> Sing b -> (a :~: b) -> GreaterThanEq a b
    , totalOrderEquivalence :: Equivalence f
    } -> TotalOrder f g

reflEquivalence :: Equivalence (:~:)
reflEquivalence = Equivalence Refl Equality.sym Equality.trans

geqReflexive :: SNat a -> SNat b -> (a :~: b) -> GreaterThanEq a b
geqReflexive SZero _ Refl = GreaterThanEqZero
geqReflexive (SSuc n) (SSuc m) Refl = GreaterThanEqSuc (geqReflexive n m Refl)

geqTrans :: SNat a -> SNat b -> SNat c
         -> GreaterThanEq a b -> GreaterThanEq b c -> GreaterThanEq a c
geqTrans _ _ _ _ GreaterThanEqZero = GreaterThanEqZero
geqTrans (SSuc sa) (SSuc sb) (SSuc sc) (GreaterThanEqSuc a) (GreaterThanEqSuc b) =
  GreaterThanEqSuc (geqTrans sa sb sc a b)

-- This is total even though GHC does not know that.
type family GeqTrans (a :: Nat) (b :: Nat) (c :: Nat) (n :: GreaterThanEq a b) (m :: GreaterThanEq b c) :: GreaterThanEq a c where
  GeqTrans a b 'Zero d 'GreaterThanEqZero = 'GreaterThanEqZero
  GeqTrans ('Suc a) ('Suc b) ('Suc c) ('GreaterThanEqSuc g) ('GreaterThanEqSuc f) =
    'GreaterThanEqSuc (GeqTrans a b c g f)

type family GeqTotal (a :: Nat) (b :: Nat) :: (Either (GreaterThanEq b a) (GreaterThanEq a b)) where
  GeqTotal 'Zero a           = 'Left 'GreaterThanEqZero
  GeqTotal ('Suc n) 'Zero    = 'Right 'GreaterThanEqZero
  GeqTotal ('Suc n) ('Suc m) = GeqTotalHelp (GeqTotal n m)

type family GeqTotalHelp (e :: Either (GreaterThanEq b a) (GreaterThanEq a b)) :: (Either (GreaterThanEq ('Suc b) ('Suc a)) (GreaterThanEq ('Suc a) ('Suc b))) where
  GeqTotalHelp ('Left gt) = 'Left ('GreaterThanEqSuc gt)
  GeqTotalHelp ('Right gt) = 'Right ('GreaterThanEqSuc gt)

-- This type family is partial
type family ForceLeft (e :: Either a b) :: a where
  ForceLeft ('Left a) = a

-- This type family is partial
type family ForceRight (e :: Either a b) :: b where
  ForceRight ('Right b) = b

-- type family GeqDecidable (a :: Nat) (b :: Nat) :: (Either (GreaterThanEq b a) (Negated (GreaterThanEq b a))) where
--   GeqDecidable 'Zero a = 'Left 'GreaterThanEqZero
--   GeqDecidable ('Suc a) 'Zero = 'Right 'Negated
--   -- GeqDecidable ('Suc a) ('Suc b) =
--
-- type family GeqDecidableHelp (e :: Either (GreaterThanEq b a) (Negated (GreaterThanEq b a))) :: (Either (GreaterThanEq ('Suc b) ('Suc a)) (Negated (GreaterThanEq ('Suc b) ('Suc a)))) where
--   GeqDecidableHelp ('Left gt) = 'Left ('GreaterThanEqSuc gt)
--   GeqDecidableHelp ('Right negated_bgta)
--   -- GeqDecidableHelp ('Right gt) = 'Right ('GreaterThanEqSuc gt)

geqTotal :: SNat a -> SNat b -> Either (GreaterThanEq b a) (GreaterThanEq a b)
geqTotal SZero _        = Left GreaterThanEqZero
geqTotal (SSuc _) SZero = Right GreaterThanEqZero
geqTotal (SSuc n) (SSuc m) =
  case geqTotal n m of
    Left gt -> Left (GreaterThanEqSuc gt)
    Right gt -> Right (GreaterThanEqSuc gt)

geqTotalOrder :: TotalOrder (:~:) GreaterThanEq
geqTotalOrder = TotalOrder geqAntisym geqTrans geqTotal geqReflexive reflEquivalence

geqAntisym :: GreaterThanEq n m -> GreaterThanEq m n -> n :~: m
geqAntisym GreaterThanEqZero GreaterThanEqZero = Refl
geqAntisym (GreaterThanEqSuc a) (GreaterThanEqSuc b) = cong (geqAntisym a b)

data Value a = Top | Bottom | Middle a

data LiftGeq :: (a -> a -> Type) -> Value a -> Value a -> Type where
  LiftGeqTop :: LiftGeq f 'Top v
  LiftGeqBottom :: LiftGeq f v 'Bottom
  LiftGeqMiddle :: f a b -> LiftGeq f ('Middle a) ('Middle b)

data OList :: (a -> a -> Type) -> Value a -> Value a -> Type where
  OListNil :: LiftGeq f upper lower -> OList f lower upper
  OListCons :: OList f ('Middle x) upper -> LiftGeq f ('Middle x) lower -> OList f lower upper

data Empty

data Negated a = UnsafeNegated
type family Absurd (e :: Empty) :: k where
type family Cheat :: Empty where

type family Insert (y :: a) (ol :: OList (f :: a -> a -> Type) l u) (gt1 :: LiftGeq f ('Middle y) l) (gt2 :: LiftGeq f u ('Middle y)) :: OList f l u where
  Insert y ('OListNil unused1) xgtl ugtx = 'OListCons ('OListNil ugtx) xgtl
  Insert y ('OListCons (xs :: OList f ('Middle x) u) xgtl) ygtl ugty = InsertHelp y x xs xgtl ygtl ugty (GenericTotal f x y)

type family InsertHelp (y :: a) (x :: a) (xs :: OList f ('Middle x) u) (xgtl :: LiftGeq f ('Middle x) l) (ygtl :: LiftGeq f ('Middle y) l) (ugty :: LiftGeq f u ('Middle y)) (e :: Either (f y x) (f x y)) :: OList f l u where
  InsertHelp y x xs xgtl ygtl ugty ('Right xgty) = 'OListCons ('OListCons xs ('LiftGeqMiddle xgty)) ygtl
  InsertHelp y x xs xgtl ygtl ugty ('Left ygtx) = 'OListCons (Insert y xs ('LiftGeqMiddle ygtx) ugty) xgtl

type family FromList (xs :: [x]) :: OList (GenericGreaterThanEq x) 'Bottom 'Top where
  FromList '[] = OListNil 'LiftGeqTop
  FromList (x ': xs) = Insert x (FromList xs) 'LiftGeqBottom 'LiftGeqTop

type family ToList (xs :: OList (f :: a -> a -> Type) l u) :: [a] where
  ToList ('OListNil unused) = '[]
  ToList ('OListCons (xs :: OList f ('Middle a) upper) unused) = a ': ToList xs

type family GenericGreaterThanEq (a :: Type) :: a -> a -> Type
type instance GenericGreaterThanEq Nat = GreaterThanEq

-- type family GenericGreaterThanEq :: a -> a -> Type
-- type instance GenericGreaterThanEq = GreaterThanEq

type family GenericTotal (f :: k -> k -> Type) (a :: k) (b :: k) :: Either (f b a) (f a b)
type instance GenericTotal GreaterThanEq (a :: Nat) (b :: Nat) = GeqTotal a b

type family CompareGtEq (x :: a) (y :: a) :: Bool

type family Demote (s :: a) :: k

type instance Demote a = DemoteNat a

type family DemoteNat (s :: SNat n) :: Nat where
  DemoteNat 'SZero = 'Zero
  DemoteNat ('SSuc s) = 'Suc (DemoteNat s)

type SingletonOne = 'OListCons ('OListNil 'LiftGeqTop) ('LiftGeqMiddle OneGreaterThanOne)
type SingletonSomething = 'OListCons ('OListNil 'LiftGeqTop) 'LiftGeqBottom
type SingletonOneAlt = Insert One ('OListNil 'LiftGeqTop) ('LiftGeqMiddle OneGreaterThanOne) 'LiftGeqTop

-- type SingletonOne = 'OListCons SOne ('OListNil 'LiftGeqTop) ('LiftGeqBottom)
--
-- type SingletonTwo = ('OListCons STwo ('OListNil 'LiftGeqTop) ('LiftGeqMiddle TwoGreaterThanOne) :: OList SNat GreaterThanEq ('Middle One) 'Top)
--
-- type TwoOne = 'OListCons SOne SingletonTwo ('LiftGeqMiddle OneGreaterThanOne)
-- -- type TwoOneAlt = Insert SOne ('OListNil 'LiftGeqTop) 'LiftGeqBottom 'LiftGeqTop
--
type OneGreaterThanOne = ('GreaterThanEqSuc 'GreaterThanEqZero :: GreaterThanEq One One)
-- type TwoGreaterThanTwo = ('GreaterThanEqSuc ('GreaterThanEqSuc 'GreaterThanEqZero) :: GreaterThanEq Two Two)
-- type TwoGreaterThanOne = ('GreaterThanEqSuc 'GreaterThanEqZero :: GreaterThanEq Two One)

type SOne = 'SSuc 'SZero
type STwo = 'SSuc ('SSuc 'SZero)

type One = 'Suc 'Zero
type Two = 'Suc ('Suc 'Zero)

type N0 = 'Zero
type N1 = 'Suc N0
type N2 = 'Suc N1
type N3 = 'Suc N2
type N4 = 'Suc N3
type N5 = 'Suc N4

cong :: forall f a b. (a :~: b) -> (f a :~: f b)
cong Refl = Refl

main :: IO ()
main = putStrLn "Hello World"

-- data OList :: (a -> Type) -> (a -> a -> Type) -> Value a -> Value a -> Type where
--   OListNil :: LiftGeq f upper lower -> OList sing f lower upper
--   OListCons :: sing x -> OList sing f ('Middle x) upper -> LiftGeq f ('Middle x) lower -> OList sing f lower upper

-- These type families cannot be written. I am stuck.
-- type family Insert (p :: (s :: k -> Type) x) (ol :: OList (s :: k -> Type) f l u) (gt1 :: LiftGeq f ('Middle x) l) (gt2 :: LiftGeq f u ('Middle x)) :: OList (s :: k -> Type) f l u where
--   Insert y ('OListNil unused1) xgtl ugtx = 'OListCons y ('OListNil ugtx) xgtl
--   Insert y ('OListCons x xs xgtl) ygtl ugty = GenericTotal y x

-- type family ToList (sing :: a -> Type) (xs :: OList sing f l u) :: [a] where
--   ToList sing ('OListNil unused) = '[]
--   ToList sing ('OListCons s xs unused) = Demote s ': ToList sing xs

-- type family ToList (xs :: OList (sing :: a -> Type) f l u) :: [a] where
--   ToList ('OListNil unused) = '[]
--   ToList ('OListCons (s :: sing a) xs unused) = a ': ToList xs