Skip to content

Instantly share code, notes, and snippets.

@paf31
Last active April 10, 2018 04:13
Show Gist options
  • Save paf31/79229a4eebbf4ba353751baeba3e867a to your computer and use it in GitHub Desktop.
Save paf31/79229a4eebbf4ba353751baeba3e867a to your computer and use it in GitHub Desktop.
module Main where
import Prelude
import Data.Exists (Exists, mkExists, runExists)
import Unsafe.Coerce (unsafeCoerce)
-- Leibniz equality:
-- Two things are equal if they are substitutable in all contexts.
type Leib a b = forall f. f a -> f b
-- A few helpers which are already provided by purescript-leibniz:
data Sym f a b = Sym (f b -> f a)
-- Leibniz equality is symmetric
sym :: forall a b. Leib a b -> Leib b a
sym f fb = let Sym g = f (Sym id) in g fb
-- Leibniz equality can be lowered. This is safe since every type
-- constructor in PureScript is injective.
lower :: forall f a b. Leib (f a) (f b) -> Leib a b
lower = unsafeCoerce
data Flip f a b = Flip (f b a)
-- Lift an equality over the first argument of a
-- two-argument type constructor.
liftLeib2 :: forall f a b c. Leib a b -> f a c -> f b c
liftLeib2 l fac = let Flip fbc = l (Flip fac) in fbc
-- In order to refute nonsensical equalities, we need an apartness
-- relation. This type class separates the two types a and b
-- (if they are indeed apart), mapping them to distinct types Unit
-- and Void via a fundep.
class Which a b c r | a b c -> r
instance which1 :: Which a b a Unit
instance which2 :: Which a b b Void
-- Now let's capture the result type of the Which fundep as a type
-- constructor. We don't have associated types, so this is the best
-- we can do, but the fundep at least guarantees the coercions are
-- safe.
data W a b c
w :: forall a b c r. Which a b c r => r -> W a b c
w = unsafeCoerce
unW :: forall a b c r. Which a b c r => W a b c -> r
unW = unsafeCoerce
-- For example, we can refute that String and Int are equal:
stringNotInt :: Leib String Int -> Void
stringNotInt l = unW (l (w unit :: W String Int String))
-- If you comment this out, it will fail, since String and String are
-- not apart.
-- stringNotString :: Leib String String -> Void
-- stringNotString l = unW (l (w unit :: W String String String))
-- Now we can write a safe zipWith function on length-indexed lists,
-- without skipping cases.
-- First, natural numbers lifted to the type level, as usual:
data Z
data S n
-- We can refute the equality of Z and S n for any n:
zIsn'tS :: forall n. Leib Z (S n) -> Void
zIsn'tS l = unW (l (w unit :: W Z (S n) Z))
-- Vectors of length n. The GADT version would be
--
-- data Vec n a where
-- Nil :: Vec Z a
-- Cons :: a -> Vec n a -> Vec (S n) a
data Vec n a
= Nil (Leib n Z)
| Cons (Exists (Cons_ n a))
data Cons_ n a m = Cons_ (Leib n (S m)) a (Vec m a)
-- Finally, here is the well-typed zipWith function:
zipWith :: forall n a b c. (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith _ (Nil l) (Nil _) = Nil l
zipWith f n@(Nil _) c = zipWith (flip f) c n
zipWith f (Cons e1) v = e1 # runExists \(Cons_ l1 a as) ->
case v of
Cons e2 -> e2 # runExists \(Cons_ l2 b bs) ->
Cons (mkExists (Cons_ l1 (f a b) (zipWith f as (liftLeib2 (lower (sym l2 >>> l1)) bs))))
-- This is the bad case, where the lengths don't match.
-- We have to refute the claim that Z = S n:
Nil l2 -> absurd (zIsn'tS (l1 <<< sym l2))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment