Skip to content

Instantly share code, notes, and snippets.

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