Skip to content

Instantly share code, notes, and snippets.

@andrewthad
Created July 8, 2016 20:22
Show Gist options
  • Save andrewthad/a5bcbba8714115955c3fe3a2946b50fd to your computer and use it in GitHub Desktop.
Save andrewthad/a5bcbba8714115955c3fe3a2946b50fd to your computer and use it in GitHub Desktop.
Type Level ordered list in haskell
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment