Sec 4.2 of Servant Paper

servant_paper_4_2.hs

--
-- Type-level Web APIs with Servant 
-- 
-- 4.2 Interpreting open type-level DSLs
--
{-# LANGUAGE TypeOperators        #-} -- for :+
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
-- Wihtout UndecidableInstances, got an error as follows: 
-- Illegal nested type family application ‘Value e1 (Value e2 r)’ 
--   (Use UndecidableInstances to permit this)
{-# LANGUAGE ScopedTypeVariables  #-}
-- Wihtout ScopedTypeVariables, got an error as follows: 
-- Couldn't match type ‘Value a0 (Value a1 r)’
--                      with ‘Value e1 (Value e2 r)’
--       Expected type: Value (e1 :+ e2) r
--         Actual type: Value a0 (Value a1 r)
--       NB: ‘Value’ is a type function, and may not be injective

import Data.Proxy

data One
data e1 :+ e2
data Hole

type Two = One :+ One
type Holes = Hole :+ One :+ Hole

class HasValue a where
  type Value a r :: *                           -- r stands for remains??
  valOf :: Proxy a -> (Int -> r) -> Value a r
--                                  ^^^^^^^^^
--                                  will change type by Type Families

instance HasValue One where
  type Value One r = r
  valOf _ ret = ret 1
-- ** Rational **
-- valOf :: Proxy a -> (Int -> r) -> Value One r
--       :: Proxy a -> (Int -> r) -> r
-- valOf    _           ret       
--                                = ret 1 :: r

instance HasValue Hole where
  type Value Hole r = Int -> r
  valOf _ ret n = ret n
-- ** Rational **
-- valOf :: Proxy a -> (Int -> r) -> Value Hole r
--       :: Proxy a -> (Int -> r) -> (Int -> r)
-- valOf    _           ret           n   
--                                        =  ret n :: r 

instance (HasValue e1, HasValue e2) => HasValue (e1 :+ e2) where
  type Value (e1 :+ e2) r = Value e1 (Value e2 r)
  valOf _ ret = valOf (Proxy :: Proxy e1) (\v1 -> valOf (Proxy :: Proxy e2) (\v2 -> ret (v1 + v2) )) 
-- ** Rational **
-- valOf :: Proxy a -> (Int -> r) -> Value (e1 :+ e2) r
--       :: Proxy a -> (Int -> r) -> Value e1 (Value e2 r)
--  ex.  e1 :: One, e2 :: Two
--       :: Proxy a -> (Int -> r) -> Value One (Value Two r)
--       :: Proxy a -> (Int -> r) -> Value One (Value (One :+ One) r)
--       :: Proxy a -> (Int -> r) -> Value One (Value One (Value One r))
--       :: Proxy a -> (Int -> r) -> Value One (Value One (r          ))
--       :: Proxy a -> (Int -> r) -> Value One (Value One  r           )
--       :: Proxy a -> (Int -> r) -> Value One (r                      )
--       :: Proxy a -> (Int -> r) -> Value One  r
--       :: Proxy a -> (Int -> r) -> r

valueOf :: HasValue a => Proxy a -> Value a Int
valueOf p = valOf p id

main :: IO ()
main = do
  let t1 = valueOf (Proxy :: Proxy Two)
  let t2 = valueOf (Proxy :: Proxy Holes)
  print (t1, t2 3 4)