Skip to content

Instantly share code, notes, and snippets.

@lylek
Last active Oct 28, 2019
Embed
What would you like to do?
STLC Pairs
{-# 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)
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment