越来越推导出类型类分辨率
问题描述:
,我们可以得到一个价值层面证明[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)())
答
没有办法将任意约束派生为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])
答
这可能是你以后的事,或者至少足以给你一个大概的想法。我想不出一种让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]
。
这确实是一个有趣的练习! – nicolas