Generalized Algebra Data Types for DSLs, with Free Monads, in F#

GADT.fsx

/// Example encoding of the shape of GADT one finds for request types
module Request =
  /// The constructors must be kept private, so that we can refine the types of
  /// the introduction rules.
  type T<'a> =
    private
    | FileExists' of string
    | ReadText' of string
    | GetCwd'

  /// Introduction rule for a query about whether a certain path represented by
  /// the string points to an existent file. This must be the ONLY way to create
  /// an instance of this case, if we are to maintain type safety.
  let FileExists : string -> T<bool> = FileExists'

  /// Introduction rule for a query that reads all the text from a file of the
  /// certain path represented by the given string, presuming it exists. This must
  /// be the ONLY way to create an instance of this case, if we are to maintain
  /// type safety.
  let ReadText : string -> T<string> = ReadText'

  /// Introduction rule for a query that, without taking any inputs, gives the
  /// current working directory of the process. This must be the ONLY way to
  /// create an instance of this case, if we are to maintain type safety.
  let GetCwd : T<string> = GetCwd'

  /// Elimination rule
  type Eliminator = {
    FileExists : string -> bool
    ReadText : string -> string
    GetCwd : unit -> string
  }

  let elim (e : Eliminator) : T<'a> -> 'a =
    function
    // For each of these cases, because we have given only one introduction
    // rule, and match it to the elimination rule, we know that the types must
    // match, and therefore it is safe to coerce them.
    | FileExists' path -> unbox (e.FileExists path)
    | ReadText' path -> unbox (e.ReadText path)
    | GetCwd' -> unbox (e.GetCwd ())

/// Example encoding of the shape of Rank 2 Type one finds when handling
/// request-type shaped GADTs, in a DSL, for example.
module Handler =
  /// data T a = forall b. Handle (Request b) (b -> a)
  type T<'a> =
    private
    | Handle' of (Request.Eliminator -> 'a)

  /// Introduction rule for the handler
  let Handle<'a,'b> (req : Request.T<'b>) (handle : 'b -> 'a) : T<'a> =
    Handle' (fun elim -> Request.elim elim req |> handle)

  /// Elimination rule for the handler. Not the full power of what you would get
  /// if you'd actually written it in Haskell with `Rank2Types` on, but good
  /// enough to be useful for executing a DSL.
  let elim (e : Request.Eliminator) : T<'a> -> 'a =
    function | Handle' f -> f e

  /// Covariant endofunctor map
  let map (f : 'a -> 'b) : T<'a> -> T<'b> =
    function | Handle' f' -> Handle' (f' >> f)

/// Freer monad over the request; though what is categorically free, is
/// expensive in F#...
module Freer =
  /// data FFree f a where -- with f constrained to Request
  ///   Pure :: a -> FFree f a
  ///   Impure :: forall x. f x -> (x -> FFree f a) -> FFree f a
  type M<'a> =
    | Pure of 'a
    | Impure' of (Request.Eliminator -> M<'a>)

  let Impure<'a,'b> (req : Request.T<'b>) (handle : 'b -> M<'a>) : M<'a> =
    Impure' (fun elim -> Request.elim elim req |> handle)

  /// Monad bind
  let rec bind (f : 'a -> M<'b>) : M<'a> -> M<'b> =
    function
    | Pure x -> f x
    | Impure' f' -> Impure' (f' >> bind f)

  let join<'a> : M<M<'a>> -> M<'a> = bind id

  /// Covariant endofunctor map
  let map (f : 'a -> 'b) : M<'a> -> M<'b> =
    bind (f >> Pure)

  /// Applicative functor apply
  let rec ap (f : M<'a -> 'b>) (x : M<'a>) : M<'b> =
    bind (fun f' -> map f' x) f

  let lift (req : Request.T<'a>) : M<'a> =
    Impure req Pure

  type FreerMonadBuilder () =
    member this.Bind (x, f) = bind f x
    member this.Return x = Pure x
    member this.ReturnFrom x = x

  let rec run (elim : Request.Eliminator) : M<'a> -> 'a =
    function
    | Pure x -> x
    | Impure' f -> run elim (f elim)

let freer = Freer.FreerMonadBuilder ()

open System.IO

let readOrDefault filename = freer {
  let! cwd = Freer.lift Request.GetCwd
  let filepath = Path.Combine (cwd, filename)
  let! exists = Freer.lift (Request.FileExists filepath)
  if exists
  then return! Freer.lift (Request.ReadText filepath)
  else return "Hello, world!"
}

module Runtime =
  let executor : Request.Eliminator = {
    FileExists = File.Exists
    ReadText = File.ReadAllText
    GetCwd = Directory.GetCurrentDirectory
  }

  let exec<'a> : Freer.M<'a> -> 'a = Freer.run executor

readOrDefault "hello-world.txt"
|> Runtime.exec
|> stdout.WriteLine