来自haskell中实例搜索的证明树

Question

无论如何要欺骗haskell（原始haskell？源插件？任何东西？）以获得类型类如何派生的证明树？

我想要什么，使用下面的例子说：

**Diff**
           --      --
           Id      Id
----       ----------
Unit       Prod Id Id
---------------------
Sum Unit (Prod Id Id) 

**Diff**
           --      --
           Id      Id
----       ----------
Unit       Prod Id Id
---------------------
Sum Unit (Prod Id Id) 

Answer 1

根据@luqui的建议，这里是你自己的类型类的草图（具有非常愚蠢的ProofTree类型）

\n

#!/usr/bin/env stack\n-- stack --resolver lts-17.10 script\n\n{-# LANGUAGE AllowAmbiguousTypes #-}\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE EmptyCase #-}\n{-# LANGUAGE EmptyDataDeriving #-}\n{-# LANGUAGE GADTs #-}\n{-# LANGUAGE RankNTypes #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE TypeApplications #-}\n{-# LANGUAGE TypeFamilies #-}\n{-# LANGUAGE UnicodeSyntax #-}\n\nmodule SOShow3 where\n-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --\nimport Data.Constraint\nimport Data.Proxy\nimport Data.Typeable\n\n-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --\n-- Proof trees\n\ndata ProofTree = Leaf String | Node1 String ProofTree | Node2 String ProofTree ProofTree | Node3 String ProofTree ProofTree ProofTree deriving (Show)\n\n-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --\n-- Universe of polynomial functors\n\ndata Zero a deriving (Show)\n\ndata Unit a = Unit deriving (Show)\n\ndata Id a = Id a deriving (Show)\n\ndata Sum s t a = Inl (s a) | Inr (t a) deriving (Show)\n\ndata Prod s t a = s a :*: t a deriving (Show)\n\nmagic :: Zero a -> b\nmagic z = case z of\n\ninstance Functor Unit where fmap f z = Unit\n\ninstance Functor Id where fmap f (Id a) = Id (f a)\n\ninstance (Functor s, Functor t) => Functor (Sum s t) where\n  fmap f s = case s of (Inl s) -> Inl (fmap f s); (Inr s) -> Inr (fmap f s)\n\ninstance (Functor s, Functor t) => Functor (Prod s t) where fmap f (s :*: t) = fmap f s :*: fmap f t\n\n-- TreeF\ntype TreeF = Sum Unit (Prod Id Id)\n\n-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --\n-- Derivatives\n\nclass Functor f => Diff f where\n  type \xce\x94 f :: * -> *\n  -- w :: Tagged f ProofTree -- without AllowAmbiguousTypes\n  w :: ProofTree\n\ninstance Diff Unit where\n  type \xce\x94 Unit = Zero\n  w = Leaf "Unit"\n\ninstance Diff Id where\n  type \xce\x94 Id = Unit\n  w = Leaf "Id"\n\ninstance (Diff f, Diff g) => Diff (Sum f g) where\n  type \xce\x94 (Sum f g) = Sum (\xce\x94 f) (\xce\x94 g)\n  w = Node2 "Sum" (w @f) (w @g)\n\ninstance (Diff f, Diff g) => Diff (Prod f g) where\n  type \xce\x94 (Prod f g) = Sum (Prod (\xce\x94 f) g) (Prod f (\xce\x94 g))\n  w = Node2 "Product" (w @f) (w @g)\n\ntype DeltaTreeF = \xce\x94 TreeF\n\n-- > :k! DeltaTreeF\n-- DeltaTreeF :: * -> *\n-- = Sum Zero (Sum (Prod Unit Id) (Prod Id Unit))\n\nmain :: IO ()\nmain = do\n  -- Prints (\xce\x94 TreeF) -- same as :k! in GHCI\n  print (typeOf (Proxy :: Proxy (\xce\x94 TreeF))) -- Proxy (* -> *) (Sum Zero (Sum (Prod Unit Id) (Prod Id Unit)))\n\n  -- TreeF verifies Diff\n  let witness :: Dict (Diff TreeF) = Dict\n  print (typeOf witness) -- Dict (Diff (Sum Unit (Prod Id Id)))\n\n  -- TreeF verifies Diff - proof tree\n  let r = w @TreeF\n  putStrLn ("Proof tree : " ++ show r) --  Node2 "Sum" (Leaf "Unit") (Node2 "Product" (Leaf "Id") (Leaf "Id"))\n

\n

欢迎评论。

\n

编辑：删除了无用的 CPS，删除了标记AllowAmbiguousTypes（尽管有名称，但相当安全，对此有很好的解释）

\n