which.purs

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))