Skip to content

Instantly share code, notes, and snippets.

@LSLeary
Created September 23, 2024 08:06
Show Gist options
  • Save LSLeary/af10f744b591796c988fda05d7dd65fa to your computer and use it in GitHub Desktop.
Save LSLeary/af10f744b591796c988fda05d7dd65fa to your computer and use it in GitHub Desktop.
Leibniz equality as a quantified constraint with safe reification and reflection
{-# 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