Created
September 23, 2024 08:06
-
-
Save LSLeary/af10f744b591796c988fda05d7dd65fa to your computer and use it in GitHub Desktop.
Leibniz equality as a quantified constraint with safe reification and reflection
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE QuantifiedConstraints | |
, UndecidableInstances | |
, AllowAmbiguousTypes | |
#-} | |
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-} | |
module LeibnizC where | |
import Leibniz | |
class (forall c. c a => c b) => a <~> b | |
instance (forall c. c a => c b) => a <~> b | |
reify :: a <~> b => a := b | |
reify = refl | |
data Dict c a = c a => Dict | |
reflect :: forall a b r. a := b -> (a <~> b => r) -> r | |
reflect aforb r = case substitute aforb (Dict @((<~>) a)) of | |
Dict -> r | |
toLeibnizC :: a ~ b => (a <~> b => r) -> r | |
toLeibnizC r = r | |
fromLeibnizC :: a <~> b => (a ~ b => r) -> r | |
fromLeibnizC r = r | |
reflC :: (a <~> a => r) -> r | |
reflC r = r | |
transC :: forall a b c r. (a <~> b, b <~> c) => (a <~> c => r) -> r | |
transC r = r | |
castC :: a <~> b => a -> b | |
castC x = x |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment