なっ派生

Question

我々は[Int]は値レベルの導出を取得するためにDict

{-# LANGUAGE ConstraintKinds, GADTs #-} 
data Dict (p :: Constraint) where 
    Dict :: p => Dict p 

と

proof = Dict :: Dict (Show [Int]) 

あり

方法を使用して表示するインスタンスを持っていることを値のレベルの証明を得ることができます、つまり証明木全体ですか？

derivation = Apply@Int(Lam a.(Show a) :=> Show [a])) (Apply(() :=> Show Int)()) 

Answer 1

任意の制約の派生をHaskell値として得る方法はありません。

私が考えることができる最も近いことは、派生があなたの考えであるかどうかをチェックしたい場合、desugarerの出力を見ることです。

ghc -ddump-ds -ddump-to-file A.hs 

関連部分は次のようになります。

-- RHS size: {terms: 2, types: 1, coercions: 0, joins: 0/0} 
irred :: Show [Int] 
[LclId] 
irred = GHC.Show.$fShow[] @ Int GHC.Show.$fShowInt 

-- RHS size: {terms: 2, types: 3, coercions: 0, joins: 0/0} 
proof :: Dict (Show [Int]) 
[LclIdX] 
proof = Cns.Dict @ (Show [Int]) irred 

もう一つは、これはには適用されないタイプや値で、もちろんどちらか、導出を反映するために、インストルメントカスタム型クラスを書くことです既存の型クラス。

{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, GADTs, DataKinds, 
    FlexibleInstances, KindSignatures, MultiParamTypeClasses, RankNTypes, 
    ScopedTypeVariables, TypeApplications, TypeOperators, 
    UndecidableInstances #-} 

import Data.Typeable 
import Data.Kind 

data (c :: [Type]) :=> (d :: Type -> Constraint) 

class MyShow a d where 
    myshow :: a -> String 

instance (d ~ ('[] :=> MyShow Int)) => MyShow Int d where 

instance (MyShow a da, d ~ ('[da] :=> MyShow [a])) => MyShow [a] d where 

myshowInstance :: forall a d. (Typeable d, MyShow a d) => TypeRep 
myshowInstance = typeRep @_ @d Proxy 

main = print (myshowInstance @[Int]) 

出力ではなくTypeRepの適切なレンダリング方法でシングルトンを経由して、例えば、良く見えるように作ることができるが、私はあなたがメインのアイデアを得る願っています。

:=> (': * (:=> ('[] *) (MyShow Int)) ('[] *)) (MyShow [Int]) 

Answer 2

これはあなたが後にしていること、または少なくともあなたに一般的な考えを与えるのに十分かもしれません。私はGHCにこれを自動的に提供させる方法を考えることはできませんが、constraintsパッケージを使用して制約を証明する一連の含意を手動で構築できます。

instance() :=> Show Intが何であれ、代わりにCharを使用しました。これは見落としの可能性があります。欠落しているインスタンスを追加するためのプルリクエストをオープンしました。

{-# LANGUAGE ConstraintKinds #-} 

import Data.Constraints 

derivation ::() :- Show [Char] 
derivation = trans showList showChar 
    where showList :: Show a :- Show [a] 
      showList = ins 

      showChar ::() :- Show Char 
      showChar = ins 

残念ながら、この値を印刷しても内派生は表示されません。ちょうど"Sub Dict"です。

derivationを明示的にTypeApplicationsと書いてみると、Data.Constraint.Forallを使ってみることができます。 Show a :- Forall ShowとForallF Show [] :- Show [a]を証明するには、さらに2つの手順が必要です。