Existentials in C# (Haskell Translation)

Existentials.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Data.Function (fix)
import Data.IORef

-- INPUT: void M(ICounter)
-- Usage: m intCounter
m :: ICounter -> IO ()
m (ICounter start next done) = do
  putStrLn "start"
  x <- newIORef start
  fix \ loop -> do
    putStrLn "done?"
    isDone <- done <$> readIORef x
    if isDone
      then do
        putStrLn "yup, bye"
      else do
        putStrLn "nope, next"
        modifyIORef' x next
        loop

-- OUTPUT: void M(ICounterWrapper)
-- Usage: m' intCounterWrapper
m' :: ICounterWrapper -> IO ()
m' wrapper = unwrap wrapper mWitness

-- Without wrapper, equivalent to taking 'ICounterWitness<void>' directly.
--
-- Usage: m'' mWitness
m'' :: ICounterWitness (IO ()) -> IO ()
m'' witness = invoke witness intCounter'

-- OUTPUT: struct MWitness : ICounterWitness<void>
mWitness :: ICounterWitness (IO ())
mWitness = ICounterWitness \ (ICounter' start next done) -> do
  putStrLn "start"
  x <- newIORef start
  fix \ loop -> do
    putStrLn "done?"
    isDone <- done <$> readIORef x
    if isDone
      then do
        putStrLn "yup, bye"
      else do
        putStrLn "nope, next"
        modifyIORef' x next
        loop

--------------------------------------------------------------------------------

-- OUTPUT: interface ICounterWrapper
--
-- Not necessary, just hides the result type.
newtype ICounterWrapper
  = ICounterWrapper { unwrap :: forall r. ICounterWitness r -> r }

-- OUTPUT: interface ICounterWitness<ResultType>
--
-- Polymorphism here makes 'T' existential from the POV of who calls 'invoke'.
newtype ICounterWitness r
  = ICounterWitness { invoke :: forall t. ICounter' t -> r }

-- INPUT:  interface ICounter<virtual T>
-- OUTPUT: interface ICounter<T>
--
-- Only difference is that we move the type parameter from an existential to a
-- universal and let the witness's polymorphism up there ↑ existentialise it.
data ICounter    where ICounter  :: forall t. { start  :: t, next  :: t -> t, done  :: t -> Bool } -> ICounter
data ICounter' t where ICounter' ::           { start' :: t, next' :: t -> t, done' :: t -> Bool } -> ICounter' t

-- INPUT:  class Counter : ICounter<int /* existential */>
-- OUTPUT: class Counter : ICounter<int /* universal   */>, ICounterWrapper
intCounter  :: ICounter
intCounter' :: ICounter' Int

-- The implementations are identical, the only difference is that one is typed
-- as an existential packing:
--
-- > pack { t = Int }
-- >   in (0 :: Int, succ :: Int → Int, (== 42) :: Int → Bool)
-- >   :: ∃t. t × (t → t) × (t → Bool)
--
-- While the other is typed as a regular old record construction:
--
-- > (0 :: Int, succ :: Int → Int, (== 42) :: Int → Bool)
-- >  :: Int × (Int → Int) × (Int → Bool)
--
intCounter  = ICounter  { start  = 0       , next  = succ, done  = (== 42) }
intCounter' = ICounter' { start' = 0 :: Int, next' = succ, done' = (== 42) }

-- Not necessary.
intCounterWrapper :: ICounterWrapper
intCounterWrapper = ICounterWrapper { unwrap = \ w -> invoke w intCounter' }