olist_broken.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)

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 Val :: x -> Type where
--   Top    :: Val a
--   Bottom :: Val a
--   Value  :: a -> Val a

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 MyType (r :: OList f (a :: Value n) b) = MyType

-- These type families cannot be written. I am stuck.
-- type family Insert (x :: Nat) (ol :: OList f l u) (gt1 :: LiftGeq f ('Middle x) l) (gt2 :: LiftGeq f u ('Middle x)) :: OList f l u where
--   Insert x ('OListNil unused1) gtxl gtux = 'OListCons ('OListNil gtux) gtxl
-- 
-- type family ToList (xs :: OList f l u) where
--   ToList ('OListNil unused) = '[]
--   ToList ('OListCons unused

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

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