Haskell Not 98
{-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} data Zero data Succ a data Plus a b data Id :: * -> * -> * where Refl :: a -> Id a a Symm :: (Id a b) -> Id b a Tran :: (Id a b) -> (Id b c) -> (Id a c) MapId :: (Id a b) -> (Id (Succ a) (Succ b)) ZeroPlus :: Id (Plus Zero a) a SuccPlus :: Id (Plus (Succ a) b) (Succ (Plus a b)) class Lemma a where lemma :: Id (Plus a Zero) a instance Lemma Zero where lemma = ZeroPlus instance (Lemma a) => Lemma (Succ a) where lemma = goal where hypo :: (Lemma b) => Id (Plus b Zero) b hypo = lemma p1 :: (Lemma b) => Id (Succ (Plus b Zero)) (Succ b) p1 = MapId hypo p2 :: (Lemma b) => Id (Plus (Succ b) Zero) (Succ (Plus b Zero)) p2 = SuccPlus goal :: (Lemma b) => Id (Plus (Succ b) Zero) (Succ b) goal = Tran p2 p1
クラウドコンピューティングの授業だったので。