STLC Pairs

Lib.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

module Lib
    ( HasDummy
    , Injectable
    , Product
    , Union
    , pair
    , fst
    , snd
    ) where

import Prelude hiding (fst, snd)
import Data.Proxy (Proxy, Proxy(..))
import Numeric.Natural (Natural)

type family Union o a b where
    Union o o o = o
    Union o o (bl -> br) = bl -> br
    Union o (al -> ar) o = al -> ar
    Union o (al -> ar) (bl -> br) = Union o al bl -> Union o ar br

class Injectable (o :: *) a c where
    inj :: Proxy o -> a -> c
    proj :: Proxy o -> c -> a

instance Injectable (o :: *) o o where
    inj _ = id
    proj _ = id

instance (Injectable o o cl, Injectable o o cr, HasDummy cl) =>
    Injectable (o :: *) o (cl -> cr)
  where
    inj proxy x = const $ inj proxy x
    proj proxy x = proj proxy $ x dummy

instance (Injectable o al cl, Injectable o ar cr) =>
    Injectable (o :: *) (al -> ar) (cl -> cr)
  where
    inj proxy x = inj proxy . x . proj proxy
    proj proxy x = proj proxy . x . inj proxy

type Product o a b = (a -> b -> Union o a b) -> Union o a b

type ProductCandidate o a b c = (a -> b -> c) -> c

pair :: (Injectable o a c, Injectable o b c) =>
    Proxy o -> a -> b -> ProductCandidate o a b c
pair _ x y = \f -> f x y

fst :: (Injectable o a c, Injectable o b c) => Proxy o -> ProductCandidate o a b c -> a
fst proxy p = proj proxy $ p $ \x y -> inj proxy x

snd :: (Injectable o a c, Injectable o b c) => Proxy o -> ProductCandidate o a b c -> b
snd proxy p = proj proxy $ p $ \x y -> inj proxy y

class HasDummy a where
    dummy :: a

instance HasDummy (a -> a) where dummy = id
instance HasDummy b => HasDummy (a -> b) where dummy = const dummy
instance HasDummy () where dummy = ()
instance HasDummy Bool where dummy = False
instance HasDummy Char where dummy = '\000'
instance HasDummy [a] where dummy = []
instance HasDummy Int where dummy = 0
instance HasDummy Word where dummy = 0
instance HasDummy Integer where dummy = 0
instance HasDummy Natural where dummy = 0
instance HasDummy Float where dummy = 0.0
instance HasDummy Double where dummy = 0.0
instance HasDummy (Maybe a) where dummy = Nothing
instance HasDummy a => HasDummy (Either a b) where dummy = Left dummy
instance (HasDummy a, HasDummy b) => HasDummy (a, b)
    where dummy = (dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c) => HasDummy (a, b, c)
    where dummy = (dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d) => HasDummy (a, b, c, d)
    where dummy = (dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e) =>
        HasDummy (a, b, c, d, e)
    where dummy = (dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f) =>
        HasDummy (a, b, c, d, e, f)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g) =>
        HasDummy (a, b, c, d, e, f, g)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h) =>
        HasDummy (a, b, c, d, e, f, g, h)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i) =>
        HasDummy (a, b, c, d, e, f, g, h, i)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j, HasDummy k) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j, k)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j, HasDummy k, HasDummy l) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j, k, l)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j, HasDummy k, HasDummy l,
        HasDummy m) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j, k, l, m)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j, HasDummy k, HasDummy l,
        HasDummy m, HasDummy n) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j, k, l, m, n)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy, dummy, dummy, dummy, dummy)
instance (HasDummy a, HasDummy b, HasDummy c, HasDummy d, HasDummy e, HasDummy f,
        HasDummy g, HasDummy h, HasDummy i, HasDummy j, HasDummy k, HasDummy l,
        HasDummy m, HasDummy n, HasDummy o) =>
        HasDummy (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)
    where dummy = (dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy, dummy,
            dummy, dummy, dummy, dummy, dummy, dummy)

Main.hs

{-# LANGUAGE TypeApplications #-}

module Main where

import Prelude hiding (fst, snd)
import Data.Proxy (Proxy, Proxy(..))
import Lib (Product, pair, fst, snd)

main :: IO ()
main = do
    let p1 = pair (Proxy @Bool) True (&&) :: Product Bool Bool (Bool -> Bool -> Bool)
    let p1l = fst (Proxy @Bool) p1
    let p1r = snd (Proxy @Bool) p1
    print p1l -- True
    print $ p1r False False -- False
    print $ p1r False True -- False
    print $ p1r True False -- False
    print $ p1r True True -- False
    let p2 = pair (Proxy @Int) (\f -> f 3) (*) :: Product Int ((Int -> Int) -> Int) (Int -> (Int -> Int))
    let p2l = fst (Proxy @Int) p2
    let p2r = snd (Proxy @Int) p2
    print $ p2l (+5) -- 8
    print $ p2r 4 6 -- 24