Dream type system

example1.dts

:: :: morphism c = c -> c -> *

:: :: morphism c -> *
:: category p =
::   { id: p a a, compose: p b c -> p a b -> p a c }

:: :: (c -> d) -> morphism c -> morphism d -> *
:: functor f i o =
::   { map: i a b -> o (f a) (f b) }

:: :: morphism c -> morphism c
:: opposite i a b = i b a

:: :: morphism c -> morphism d -> morphism (c, d)
:: product c d (a, b) (s, t) = (c a s, d b t)

:: :: morphism c -> ((c, c) -> *) -> *
:: profunctor c p = functor p (product (opposite c) c) (->)

:: :: (a -> b -> c) -> (a, b) -> c
:: uncurry f (a, b) = f a b

:: :: morphism * -> *
:: setProfunctor p = profunctor (->) (Uncurry p)

-- We can inline this step by step to see what type we get
-- > profunctor (->) (uncurry p)
--
-- > functor (uncurry p) x (->)
--   where
--   x = product (opposite (->)) (->)
--     = \(a, b) (s, t) -> (opposite (->) a s, (->) b t)
--     = \(a, b) (s, t) -> ((->) s a, (->) b t)
--     = \(a, b) (s, t) -> (s -> a, b -> t)
--
-- > { map: i a b -> o (f a) (f b) }
--   where
--   f = uncurry p
--   i = x
--   o = (->)
--   x = \(a, b) (s, t) -> (s -> a, b -> t)
--
-- > { map: x (a, b) (s, t) -> f (a, b) -> f (s, t) }
--   where
--   f = uncurry p
--   x = \(a, b) (s, t) -> (s -> a, b -> t)
--
-- > { map: (s -> a, b -> t) -> p a b -> p s t }

:: setProfunctor (->)
fnProfunctor = { map: \(l, r) f -> r . f . l }

example2.dts

:: :: morphism c = c -> c -> *        -- kind definitions, and ...

:: :: morphism c -> *                 -- ... kind annotations go in this level
:: category p = { id, compose }       -- type definitions and ...
::   where
::   id = p a a
::   compose = p b c -> p a b -> p a c

:: category (->)                      -- ... type annotations go in this level
fnCategory = { id, compose }          -- value definitions go in this level
 where
 id x = x
 compose bc ab x = bc $ ab $ x