Proof-tree from instance search in haskell

user_242189 0
Viewed 133

Is there anyway to trick haskell (raw haskell ? source plugins ? anything ?) to get a proof tree of how a type class was derived ?

What I would like, says using the exemple below :

**Diff**
           --      --
           Id      Id
----       ----------
Unit       Prod Id Id
---------------------
Sum Unit (Prod Id Id) 

#!/usr/bin/env stack
-- stack --resolver lts-17.10 script

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}

module SOShow where

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
import Data.Constraint
import Data.Typeable

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- universe of polynomial functors

data Zero a deriving (Show)

data Unit a = Unit deriving (Show)

data Id a = Id a deriving (Show)

data Sum s t a = Inl (s a) | Inr (t a) deriving (Show)

data Prod s t a = s a :*: t a deriving (Show)

magic :: Zero a -> b
magic z = seq z (error "This is magic")

instance Functor Unit where fmap f z = Unit

instance Functor Id where fmap f (Id a) = Id (f a)

instance (Functor s, Functor t) => Functor (Sum s t) where
  fmap f s = case s of (Inl s) -> Inl (fmap f s); (Inr s) -> Inr (fmap f s)

instance (Functor s, Functor t) => Functor (Prod s t) where fmap f (s :*: t) = fmap f s :*: fmap f t

-- TreeF

type TreeF = Sum Unit (Prod Id Id)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- Derivatives

class Functor f => Diff f where
  type Δ f :: * -> *
  posns :: f a -> f (a, Δ f a)
  plug :: (a, Δ f a) -> f a

instance Diff Unit where
  type Δ Unit = Zero
  posns Unit = Unit
  plug (a, z) = magic z

instance Diff Id where
  type Δ Id = Unit
  posns (Id a) = Id (a, Unit)
  plug (a, Unit) = Id a

instance (Diff f, Diff g) => Diff (Sum f g) where
  type Δ (Sum f g) = Sum (Δ f) (Δ g)
  posns (Inl (x :: f a)) = Inl (fmap (\(a, dx) -> (a, Inl dx)) (posns x :: f (a, Δ f a)))
  posns (Inr y) = Inr (fmap (\(a, dy) -> (a, Inr dy)) (posns y))
  plug (a, Inl (x :: Δ f a)) = Inl (plug (a, x) :: f a)
  plug (a, Inr y) = Inr (plug (a, y))

instance (Diff f, Diff g) => Diff (Prod f g) where
  type Δ (Prod f g) = Sum (Prod (Δ f) g) (Prod f (Δ g))
  posns (x :*: y) = fmap (\(a, dx) -> (a, Inl (dx :*: y))) (posns x) :*: fmap (\(a, dy) -> (a, Inr (x :*: dy))) (posns y)
  plug (a, Inl (dx :*: y)) = plug (a, dx) :*: y
  plug (a, Inr (x :*: dy)) = x :*: plug (a, dy)

type B = Δ TreeF

-- > :k! B
-- B :: * -> *
-- = Sum Zero (Sum (Prod Unit Id) (Prod Id Unit))

w :: Dict (Diff TreeF) = Dict

main :: IO ()
main = do
  print w --Dict
  print (typeOf w) -- Dict (Diff (Sum Unit (Prod Id Id)))

{-
**Diff**
           --      --
           Id      Id
----       ----------
Unit       Prod Id Id
---------------------
Sum Unit (Prod Id Id)
-}
haskell
1 Answers

Based on the suggestion of @luqui, here's a sketch of what it could look like, for your own typeclasses (with a very dumb ProofTree type)

#!/usr/bin/env stack
-- stack --resolver lts-17.10 script

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}

module SOShow3 where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
import Data.Constraint
import Data.Proxy
import Data.Typeable

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- Proof trees

data ProofTree = Leaf String | Node1 String ProofTree | Node2 String ProofTree ProofTree | Node3 String ProofTree ProofTree ProofTree deriving (Show)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- Universe of polynomial functors

data Zero a deriving (Show)

data Unit a = Unit deriving (Show)

data Id a = Id a deriving (Show)

data Sum s t a = Inl (s a) | Inr (t a) deriving (Show)

data Prod s t a = s a :*: t a deriving (Show)

magic :: Zero a -> b
magic z = case z of

instance Functor Unit where fmap f z = Unit

instance Functor Id where fmap f (Id a) = Id (f a)

instance (Functor s, Functor t) => Functor (Sum s t) where
  fmap f s = case s of (Inl s) -> Inl (fmap f s); (Inr s) -> Inr (fmap f s)

instance (Functor s, Functor t) => Functor (Prod s t) where fmap f (s :*: t) = fmap f s :*: fmap f t

-- TreeF
type TreeF = Sum Unit (Prod Id Id)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- Derivatives

class Functor f => Diff f where
  type Δ f :: * -> *
  -- w :: Tagged f ProofTree -- without AllowAmbiguousTypes
  w :: ProofTree

instance Diff Unit where
  type Δ Unit = Zero
  w = Leaf "Unit"

instance Diff Id where
  type Δ Id = Unit
  w = Leaf "Id"

instance (Diff f, Diff g) => Diff (Sum f g) where
  type Δ (Sum f g) = Sum (Δ f) (Δ g)
  w = Node2 "Sum" (w @f) (w @g)

instance (Diff f, Diff g) => Diff (Prod f g) where
  type Δ (Prod f g) = Sum (Prod (Δ f) g) (Prod f (Δ g))
  w = Node2 "Product" (w @f) (w @g)

type DeltaTreeF = Δ TreeF

-- > :k! DeltaTreeF
-- DeltaTreeF :: * -> *
-- = Sum Zero (Sum (Prod Unit Id) (Prod Id Unit))

main :: IO ()
main = do
  -- Prints (Δ TreeF) -- same as :k! in GHCI
  print (typeOf (Proxy :: Proxy (Δ TreeF))) -- Proxy (* -> *) (Sum Zero (Sum (Prod Unit Id) (Prod Id Unit)))

  -- TreeF verifies Diff
  let witness :: Dict (Diff TreeF) = Dict
  print (typeOf witness) -- Dict (Diff (Sum Unit (Prod Id Id)))

  -- TreeF verifies Diff - proof tree
  let r = w @TreeF
  putStrLn ("Proof tree : " ++ show r) --  Node2 "Sum" (Leaf "Unit") (Node2 "Product" (Leaf "Id") (Leaf "Id"))

Comments welcome.

Edit : removed useless CPS, removed Tagged with AllowAmbiguousTypes (quite safe despite the name, nice explanation here on this)

user_2421890
Related