手抜きした
{-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} data Zero where Zero :: Zero data Succ a where Succ :: (Nat a) => a -> Succ a class Nat a instance Nat Zero instance (Nat a) => Nat (Succ a) data TNil data Tree a left right where Nil :: Tree b TNil TNil Node :: a -> Tree a ll lr -> Tree a rl rr -> Tree a (Tree a ll lr) (Tree a rl rr) instance Show (Tree b TNil TNil) where show Nil = "nil" instance (Show a,Show (Tree a ll lr),Show (Tree a rl rr)) => Show (Tree a (Tree a ll lr) (Tree a rl rr)) where show (Node v l r) = "{ " ++ show v ++ " | " ++ show l ++ " , " ++ show r ++ " }" type family TreeMap newT l type instance TreeMap newT TNil = TNil type instance TreeMap newT (Tree a left right) = Tree newT (TreeMap newT left) (TreeMap newT right) treeMap :: (a -> b) -> Tree a left right -> Tree b (TreeMap b left) (TreeMap b right) treeMap f Nil = Nil treeMap (f :: a -> b) (Node v l r :: Tree a left right) = goal where g :: (Tree a ll lr ~ left) => Tree a ll lr -> Tree b (TreeMap b ll) (TreeMap b lr) g tr = (treeMap f tr :: TreeMap b left) h :: (Tree a rl rr ~ right) => Tree a rl rr -> Tree b (TreeMap b rl) (TreeMap b rr) h tr = (treeMap f tr :: TreeMap b right) {- (Tree a ll lr ~ left)で TreeMap b left => TreeMap b (Tree a ll lr) => Tree b (TreeMap b ll) (TreeMap b lr) -} goal :: Tree b (TreeMap b left) (TreeMap b right) goal = Node (f v) (g l) (h r) leftsubtree :: Tree a l r -> l leftsubtree (Node a l r) = l rightsubtree :: Tree a l r -> r rightsubtree (Node a l r) = r leaf v = Node v Nil Nil tree1 = leaf (1 :: Int) tree2 = leaf (2 :: Int) tree3 = Node 3 tree1 tree2 tree4 = leaf (4 :: Int) tree5 = Node 5 tree3 tree4 tree1_ :: Tree Int (Tree Int TNil TNil) (Tree Int TNil TNil) tree1_ = treeMap pred tree1 tree3_ = treeMap show tree3 tree5_ = treeMap succ tree5
眠いので寝ます。