1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 | {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} import GHC.Prim data Mark c (d1 :: * -> Constraint) (d2 :: * -> Constraint) d t where Mark :: (c d1 d2, d t) => t -> Mark c d1 d2 d t data Tree c d a where Leaf :: Maybe (Mark c d d d t) -> a -> Tree c d a Node :: Maybe (Mark c d1 d2 d t) -> Tree c d1 a -> Tree c d2 a -> Tree c d a alterTree :: (forall c d. Tree c d a -> Tree c d a) -> Tree (~) ((~) t) a -> Tree (~) ((~) t) a alterTree f x = f x |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} import GHC.Prim data Mark c (d1 :: * -> Constraint) (d2 :: * -> Constraint) d t where Mark :: (c d1 d2, d t) => t -> Mark c d1 d2 d t data Tree c d a where OldLeaf :: (c d1 d, d1 t, d t) => a -> t -> Tree c d a NewLeaf :: a -> Tree c d a Node :: Maybe (Mark c d1 d2 d t) -> Tree c d1 a -> Tree c d2 a -> Tree c d a alterTree :: (forall c d. Tree c d a -> Tree c d a) -> Tree (~) ((~) t) a -> Tree (~) ((~) t) a alterTree f x = f x |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 | {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} import GHC.Prim -- a predicate would suffice, but is there a universal Universal :: * -> Constraint? data Mark c t where Mark :: c t t => Mark c t data Node' t data Leaf' t1 t2 t data Tree c t a where Leaf :: Maybe (Mark c (Node' t)) -> a -> Tree c t a Node :: Maybe (Mark c (Leaf' t1 t2 t)) -> Tree c t1 a -> Tree c t2 a -> Tree c t a alterTree :: (forall c t. Tree c t a -> Tree c t a) -> Tree (~) t a -> Tree (~) t a alterTree f x = f x |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 | {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} import GHC.Prim data Mark c t t' where Mark :: c t t' => Mark c t t' data Node' data Leaf' t1 t2 data Tree c t a where Leaf :: Maybe (Mark c Node' t) -> a -> Tree c t a Node :: Maybe (Mark c (Leaf' t1 t2) t) -> Tree c t1 a -> Tree c t2 a -> Tree c t a alterTree :: (forall c t. Tree c t a -> Tree c t a) -> Tree (~) t a -> Tree (~) t a alterTree f x = f x deriving instance Show (Mark c t t') deriving instance Show a => Show (Tree c t a) instance Functor (Tree c t) where fmap f (Leaf m a) = Leaf m (f a) fmap f (Node m l r) = Node m (fmap f l) (fmap f r) ex = alterTree (fmap succ) (Node (Just Mark) (Leaf (Just Mark) 1) (Leaf (Just Mark) 2)) |