A touch of GADT

{-# LANGUAGE GADTs, KindSignatures #-}

module E2
       ( Value(..), Expr(..)
       )
where

import System.IO

data In
data Out
data InOut
data Exe

data Mode :: * -> * where
  In :: Mode In
  Out :: Mode Out
  InOut ::  Mode InOut
  Exe :: Mode Exe

data OpenFile a = OpenFile Handle

data Value a where
  File :: FilePath -> Mode a -> Value (Mode a)
  Double :: Double -> Value Double
  Int :: Integer -> Value Integer
  String :: String -> Value String
  Handle :: Handle -> Mode a -> Value (OpenFile a)

-- probably deBruijn is the way to go; see
-- http://www.cse.unsw.edu.au/~chak/haskell/term-conv/

data Ix env t where
  ZeroIx ::             Ix (env, t) t
  SuccIx :: Ix env t -> Ix (env, s) t



data Expr :: * -> * -> * where  -- context, type
  RunTo :: Expr c (Mode Exe) -> Expr c [String] -> Expr c (Mode Out) -> Expr c (IO ())
  Open :: Expr c (Mode a) -> Expr c (IO (OpenFile a))
  Apply :: Expr c (a -> b) -> Expr c a -> Expr c b
  Lambda :: Expr (c, tau) b -> Expr c (tau -> b) -- maybe de Bruijn?
  Var :: Ix c a -> Expr c a
  Lit :: Value a -> Expr c a


-----------------------------------------------------
  -- more from M. Chakravarty

  -- Valuation for a type environment
--
data Val env where
  Empty :: Val ()
  Push  :: Val env -> t -> Val (env, t)

-- Projection of a value from a valuation using a de Bruijn index
--
prj :: Ix env t -> Val env -> t
prj ZeroIx      (Push val v) = v
prj (SuccIx ix) (Push val _) = prj ix val

run :: Val context -> Expr context a -> a
run rho (Var ix) = prj ix rho
run rho (Apply f x) = run rho f (run rho x)
run rho (Lambda body) = \x -> run (Push rho x) body

class Writeable a where -- File value constructors must be private
  openOut :: Value (Mode a) -> IO Handle

instance Writeable Out where
  openOut (File s Out) = openFile s WriteMode

instance Writeable InOut where
  openOut (File s InOut) = openFile s WriteMode


type Name = String