leibniz.hs

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}

-- Leibniz idea copied from:
-- http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/

newtype a :~: b = Leibniz (forall f. f a -> f b)

refl :: a :~: a
refl = Leibniz id

coe :: a :~: b -> f a -> f b
coe (Leibniz l) = l

newtype Identity a = Identity { runIdentity :: a }

coerce :: a :~: b -> a -> b
coerce (Leibniz l) = runIdentity . l . Identity

newtype Flip f a b = Flip { unFlip ::  f b a }

symm :: a :~: b -> b :~: a
symm p = unFlip (coe p (Flip refl))

-- Try to Implement polymorphic defunctionalisation without GADTs

-- This required ConstraintKinds which feels like cheating!
newtype c :=>: a = Instance (c a => ())

witness :: c :=>: a
witness = Instance ()

-- I want to a way to use the constraint witness to add the contraint to type
-- This is the wrong type, as 'a' will unify with 'b' which applies the constraint 'c'
-- to 'a' - which we obviously can't satisfy. Hopefully this give an intuition
-- as to what I'm trying to do though.
constrain :: c a => c :=>: b -> b -> (a, b :~: a)
constrain _ = undefined 

{-

data a ~> b where
  Show :: Show a => a ~> String

lower :: a ~> b -> a -> b
lower Show = show

-}

mapF :: a ~> b -> [a] -> [b]
mapF t [] = []
mapF t (x : xs) = (lower t) x : mapF t xs

data a ~> b
  = Plus1 (a :~: Int) (b :~: Int)
  | Show (Show :=>: a) (b :~: String)

lower :: a ~> b -> a -> b
lower (Plus1 pa pb) x = (coerce . symm) pb $ x' + 1 
  where
    x' = coerce pa x -- :: Int
lower (Show c p) x = (coerce . symm) p $ show b
  where
    (b, p') = constrain c x

ex1 :: [Int]
ex1 = mapF (Plus1 refl refl) [1..10]

ex2 :: [String]
ex2 = mapF (Show witness refl) [1..10]