TypeWitness.purs

module TypeWitness where 

import Prelude

import Data.Exists (Exists)
import Data.Foldable (find)
import Data.Leibniz (type (~))
import Data.Maybe (Maybe(..))
import Data.Tuple (Tuple(..))
import Data.Tuple.Nested (Tuple3, T3, (/\))
import Effect (Effect)
import Effect.Exception (throw)
import Type.Data.Row (RProxy(..))

foreign import kind UserPrivilege
-- User privileges for our users
foreign import data Member :: UserPrivilege 
foreign import data Admin :: UserPrivilege 
foreign import data Guest :: UserPrivilege 

data UserProxy (u :: UserPrivilege) = UserProxy 

-- Our type witness
data WitnessPrivilege up 
    = WitnessMember (UserProxy Member ~ up)
    | WitnessGuest  (UserProxy Guest ~ up)
    | WitnessAdmin  (UserProxy Admin ~ up)

witnessMember = WitnessMember identity 
witnessGuest = WitnessGuest identity
witnessAdmin = WitnessAdmin identity

-- Our user type
data User (up :: UserPrivilege) = User
  { id :: Int
  , name :: String
  , privilege :: WitnessPrivilege (UserProxy up)
  }

-- The type that we use to hide the privilege type variable    <-- not sure how to translate this in PS
data SomeUser where
  SomeUser :: User a -> SomeUse

-- A function that accept a user id (Integer), and reads
-- the corresponding user from the database. Note that the return
-- type level privilege is hidden in the return value `SomeUser`.
-- readUser :: Int -> Effect SomeUser
-- readUser id = pure $ case find (((==) id) <<< (\(Tuple a _) -> a)) dbRows of
--   Just (Tuple id (Tuple name type_)) -> case type_ of
--       "member" -> SomeUser (Tuple (User { id, name,  privilege: witnessMember}) identity)
--       "guest" -> SomeUser (User { id, name,  privilege: witnessGuest})
--       "admin" -> SomeUser (User { id, name,  privilege: witnessAdmin})
--   Nothing -> throw "User not found"


dbRows :: Array (T3 Int String String)
dbRows =
  [ 10 /\ "John" /\ "member"
  , 11 /\ "alice" /\ "guest"
  , 12 /\ "bob" /\ "admin"
  ]

TypeWitness2.purs

module TypeWitness where 

import Prelude

import Data.Exists (Exists)
import Data.Foldable (find)
import Data.Leibniz (type (~))
import Data.Maybe (Maybe(..))
import Data.Tuple (Tuple(..))
import Data.Tuple.Nested (Tuple3, T3, (/\))
import Effect (Effect)
import Effect.Class.Console (log, logShow)
import Effect.Exception (throw)
import Type.Data.Row (RProxy(..))
import Unsafe.Coerce (unsafeCoerce)

foreign import kind UserPrivilege
-- User privileges for our users
foreign import data Member :: UserPrivilege 
foreign import data Admin :: UserPrivilege 
foreign import data Guest :: UserPrivilege 

data UserProxy (u :: UserPrivilege) = UserProxy 

-- Our type witness
data WitnessPrivilege up 
    = WitnessMember (UserProxy Member ~ up)
    | WitnessGuest  (UserProxy Guest ~ up)
    | WitnessAdmin  (UserProxy Admin ~ up)

instance showWitnessPrivilege :: Show (WitnessPrivilege up) where 
    show = case _ of
        (WitnessMember _) -> "Member"
        (WitnessGuest _)  -> "Guest" 
        (WitnessAdmin _)  -> "Admin"

witnessMember = WitnessMember identity 
witnessGuest = WitnessGuest identity
witnessAdmin = WitnessAdmin identity

-- Our user type
newtype User (up :: UserPrivilege) = User
  { id :: Int
  , name :: String
  , privilege :: WitnessPrivilege (UserProxy up)
  }

derive newtype instance showUser :: Show (User up)

data SomeUser

-- Declare a constructor with a coercion
mkSomeUser :: forall a. User a -> SomeUser
mkSomeUser = unsafeCoerce

-- Declare an eliminator with a coercion
unSomeUser :: forall up. SomeUser -> (User up)
unSomeUser = unsafeCoerce <<< identity

-- A function that accept a user id (Integer), and reads
-- the corresponding user from the database. Note that the return
-- type level privilege is hidden in the return value `SomeUser`.
readUser :: Int -> Effect SomeUser
readUser id' = case find (((==) id') <<< (\(Tuple a _) -> a)) dbRows of
  Just (Tuple id (Tuple name type_)) -> case type_ of
      "member" -> pure $ mkSomeUser (User { id, name,  privilege: witnessMember})
      "guest" -> pure $ mkSomeUser (User { id, name,  privilege: witnessGuest})
      "admin" -> pure $ mkSomeUser (User { id, name,  privilege: witnessAdmin})
      _       -> throw $ "privilege not found"
  Nothing -> throw "User not found" 


main :: Effect Unit
main = do
    user <- unSomeUser <$> readUser 10
    logShow user

dbRows :: Array (T3 Int String String)
dbRows =
  [ 10 /\ "John" /\ "member"
  , 11 /\ "alice" /\ "guest"
  , 12 /\ "bob" /\ "admin"
  ]