obtenir dérivations sur classe de types résolution

Question

Nous pouvons obtenir une preuve de niveau de valeur que [Int] a une instance Afficher l'aide d'un Dict

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

et

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

Y at-il un moyen d'obtenir une dérivation de niveau de valeur , c'est-à-dire l'arbre de preuve entier?

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

Answer 1

Il n'existe aucun moyen d'obtenir la dérivation d'une contrainte arbitraire en tant que valeur Haskell. La chose la plus proche à laquelle je peux penser, si vous voulez vérifier si la dérivation est ce que vous pensez qu'elle est, est de regarder la sortie desugarer.

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

La partie pertinente ressemble à ceci:

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

Un autre est d'écrire sur mesure instrumenté pour classes de types de refléter la dérivation, soit dans des types ou des valeurs, mais bien sûr, cela ne vaut pas classes de types préexistantes.

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

La sortie pourrait être fait pour regarder mieux, par exemple, au moyen d'un singleton avec une méthode de rendu appropriée au lieu de TypeRep, mais je l'espère, vous obtenez l'idée principale.

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

Answer 2

Ceci peut être ce que vous cherchez, ou au moins assez pour vous donner une idée générale. Je ne peux pas imaginer un moyen d'avoir GHC automatiquement, mais vous pouvez construire manuellement la chaîne d'implication qui prouve la contrainte en utilisant le paquet constraints.

Pour une raison quelconque, il n'y a pas instance() :=> Show Int, donc j'ai utilisé Char à la place. C'est probablement un oubli, j'ai ouvert une demande de tirage pour ajouter les instances manquantes.

{-# 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 

impression Malheureusement cette valeur ne montre pas les dérivations internes, juste "Sub Dict".

Un exercice amusant pourrait être d'essayer d'écrire derivation avec explicite TypeApplications en utilisant Data.Constraint.Forall. Vous aurez besoin de quelques étapes supplémentaires pour prouver Show a :- Forall Show et ForallF Show [] :- Show [a].