Last active

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

Skew binary tree with the invariants enforced by the type system, using a nested data type.

View skewbintree.hs
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
{-# LANGUAGE GADTs #-}
 
type Id = Int
 
data Path a where
P :: P a -> Path a
Two :: b -> b -> P (Br b) -> (P (Br b) -> P a) -> Path a
data Br a = Br a Id a
data P a = Nil | Zero (P (Br a)) | One a (P (Br a))
 
cons :: Id -> Path Id -> Path Id
cons x (P p) = consP x p
cons x (Two y z zs f) = case consP (Br y x z) zs of
P p -> P (f p)
Two y' z' zs' f' -> Two y' z' zs' (f . f')
 
consP :: a -> P a -> Path a
consP x Nil = P $ One x Nil
consP x (Zero xs) = P $ One x xs
consP x (One y xs) = Two x y xs Zero
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.