越来越推导出类型类分辨率

，我们可以得到一个价值层面证明[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

越来越推导出类型类分辨率

回答

相关问题