1
Fork 0
tagless-final-parsing/leibniz-proof/app/Main.hs

29 lines
738 B
Haskell
Raw Normal View History

2021-12-20 13:16:50 +00:00
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE TypeOperators #-}
module Main where
import Data.Eq.Type ((:=)(..), refl)
newtype F1 t b a = F1 {runF1 :: t := (a -> b)}
newtype F2 t a b = F2 {runF2 :: t := (a -> b)}
functionEquality
:: forall a1 a2 b1 b2
. a1 := a2
-> b1 := b2
-> (a1 -> b1) := (a2 -> b2)
functionEquality
(Refl s1) -- s1 :: forall c. c a1 -> c a2
(Refl s2) -- s2 :: forall c. c b1 -> c b2
= runF2 -- (a1 -> b1) := (a2 -> b2)
. s2 -- F2 (a1 -> b1) a2 b2
. F2 -- F2 (a1 -> b1) a2 b1
. runF1 -- (a1 -> b1) := (a2 -> b1)
. s1 -- F1 (a1 -> b1) b1 a2
. F1 -- F1 (a1 -> b1) b1 a1
$ refl -- (a1 -> b1) := (a1 -> b1)
main :: IO ()
main = putStrLn "Hello, Haskell!"