越來越推導出類型類分辨率

，我們可以得到一個價值層面證明[Int]具有使用Dict越來越推導出類型類分辨率

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

和

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

有沒有辦法得到一個值水平推導一個顯示實例，那就是整個證明樹？

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

來源

2017-10-18 nicolas

沒有辦法將任意約束派生爲Haskell值。

我能想到的最接近的事情是，如果你想檢查派生是否是你認爲的那樣，就是看清楚輸出。

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])

來源

2017-10-18 10:46:40

這可能是你以後的事，或者至少足以給你一個大概的想法。我想不出一種讓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]。

來源

2017-10-18 19:49:54 cdk

這確實是一個有趣的練習！ – nicolas

越來越推導出類型類分辨率

回答

相關問題