public
Last active

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

  • Download Gist
skewbintree.hs
Haskell
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

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.