CODEWITHSUNDEEP
haskellconstraintstypeclass
nicolas
nicolas

Reputation: 9815

getting derivations out of typeclass resolution

We can get a value level proof that [Int] has a Show instance using a Dict 

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

and 

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

Is there a way to get a value level derivation, that is, the entire proof tree ?

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

Upvotes: 4

Views: 94

Answers (2)

cdk
cdk

Reputation: 6778

This may be what you're after, or at least enough to give you a general idea. I can't think of a way to have GHC provide this automatically, but you can manually construct the chain of entailments that proves the constraint using the constraints package.

For whatever reason, there is no instance () :=> Show Int, so I've used Char instead. This is likely an oversight, I've opened a pull request to add the missing instances.

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

Unfortunately printing this value doesn't show the inner derivations, just "Sub Dict".

A fun exercise could be to try to write derivation with explicit TypeApplications using Data.Constraint.Forall. You'll need a couple extra steps to prove Show a :- Forall Show and ForallF Show [] :- Show [a].

Upvotes: 1

Li-yao Xia
Li-yao Xia

Reputation: 33509

There isn't a way to get the derivation of an arbitrary constraint as a Haskell value.

The closest thing I can think of, if you want to check whether the derivation is what you think it is, is to look at the desugarer output.

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

The relevant part looks like this:

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

Another one is to write custom typeclasses instrumented to reflect the derivation, either in types or in values, but of course this doesn't apply to preexisting type classes.

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

The output could be made to look better, e.g., via a singleton with a proper rendering method instead of TypeRep, but I hope you get the main idea.

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

Upvotes: 4

Related Questions