Constrained Trees

ConstraintTrees.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
module ConstraintTrees where

import Data.Type.Equality

type family If (p :: Bool) (a :: k) (b :: k) :: k where
  If 'True a b = a
  If 'False a b = b

type family Remove (k :: a) (ks :: [*]) :: [*] where
  Remove k (l ': ls) = If (k == l) ls (l ': Remove k ls)

type family (xs :: [*]) :++ (ys :: [*]) :: [*] where
  '[] :++ as = as
  (a ': as) :++ bs = as :++ (a ': bs)

data ConstraintTree requires provides x where
  Leaf :: ConstraintTree '[] '[] x
  BlankNode :: x
            -> ConstraintTree reqA provA x
            -> ConstraintTree reqB provB x
            -> ConstraintTree (reqA :++ reqB) (provA :++ provB) x
  ReqNode :: req
          -> x
          -> ConstraintTree reqA provA x
          -> ConstraintTree reqB provB x
          -> ConstraintTree (req ': (reqA :++ reqB)) (provA :++ provB) x
  ProvNode :: prov
           -> x
           -> ConstraintTree reqA provA x
           -> ConstraintTree reqB provB x
           -> ConstraintTree (reqA :++ reqB) (prov ': (provA :++ provB)) x


class ValidTree a where
  validate :: a -> a
  validate = id

instance ValidTree (ConstraintTree '[] '[] x)
instance ValidTree (ConstraintTree (Remove p rs) ps x) => ValidTree (ConstraintTree rs (p ': ps) x)

data Foo = Foo
data Bar = Bar
data Baz = Baz

tree1 = validate $
        BlankNode "a"
        ( ReqNode Foo "b"
          (ProvNode Foo "c" Leaf Leaf)
          (BlankNode "d" (ReqNode Bar "e" Leaf Leaf) Leaf)
        )
        (ProvNode Bar "f" Leaf Leaf)

-- `validate tree2` will fail to typecheck, due to the unmet requirement of Baz
tree2 = -- validate $
        BlankNode "a"
        ( ReqNode Foo "b"
          (ProvNode Foo "c" Leaf Leaf)
          (BlankNode "d" (ReqNode Bar "e" Leaf Leaf) Leaf)
        )
        ( ProvNode Bar "f" Leaf
          (ReqNode Baz "g" Leaf Leaf)
        )