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)
-}
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)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With