Example of Embedded Domain Specific Type Systems for Declarative EDSLs

Foos.idr

-- ---------------------------------------------------------------- [ Foos.idr ]
-- Module    : Foos.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : GPL v3
--             see http://choosealicense.com/licenses/gpl-3.0/
-- --------------------------------------------------------------------- [ EOH ]

||| Example of Embedded Domain Specific Type Systems for Declarative EDSLs
|||
||| This example represents the `FooExpr` language, this is a
||| declarative language for specifiying different kinds of elements,
||| and their links.  The real world semantics of `FooExpr` do nto
||| matter here, but think of we are building graphs and constraining
||| the values for nodes and edges.
module Foos

-- DList, is a custom data type for collecting values of a dependent
-- type. See http://www.github.com/jfdm/idris-containers for more
-- information. DList allows for the witness of a dependent pair to be
-- collected and externalised in the type.
import public Data.Sigma.DList

-- -------------------------------------------------- [ The Meta Typing System ]

||| Meet the meta-types in our typing system.
data ATy = A | B | C | D
data WTy = W | X | Y | Z

||| Meet the types in our type system.
data FooTy = Foo ATy | Bar WTy | FooBarTy | BarFooTy

||| Meet the types for nodes and edges.
data StructTy = ELEM | LINK

-- ----------------------------------------- [ Some External Typing Judgements ]

||| For links of type `FooBar` that connects a foo to a bar the
||| following set of links are permissible.
data ValidFB : ATy -> WTy -> Type where
  AW : ValidFB A W
  BX : ValidFB B X

||| The typing judgements to determine what a valid `FooBar` link
||| consists of.
data ValidFooBar : FooTy -> FooTy -> Type where
  ||| A Foo can connect a Bar iff it is a valid FB link.
  FooBarFB : {auto prf : ValidFB x y} -> ValidFooBar (Foo x) (Bar y)
  ||| Any Foo can connect to any Foo.
  FooBarFF : ValidFooBar (Foo x) (Foo y)

||| Any Bar nodes can connect to a foo node.
data ValidBarFoo : FooTy -> FooTy -> Type where
  BarFooBF : ValidBarFoo (Bar x) (Foo y)

||| A single bar node can connect to manny foo nodes.
data ValidBarFoos : FooTy -> List FooTy -> Type where
  Nil  : ValidBarFoos x Nil
  (::) : (x : FooTy)
      -> (y : FooTy)
      -> {auto prf : ValidBarFoo x y}
      -> ValidBarFoos x ys
      -> ValidBarFoos x (y::ys)

-- -------------------------------------------------- [ Well-Typed Expressions ]

||| The language of `FooExpr`
data FooExpr : FooTy -> StructTy -> Type where

  ||| Create a node of type Foo
  FooNode : (ty : ATy) -> String -> FooExpr (Foo ty) ELEM

  ||| Create a node of type Bar
  BarNode : (ty : WTy) -> String -> Maybe Nat -> FooExpr (Bar ty) ELEM

  ||| Create a valid FooBar link.
  FooBar  : FooExpr x ELEM
         -> FooExpr y ELEM
         -> {auto prf : ValidFooBar x y}  -- Enforce typing judgement
         -> FooExpr FooBarTy LINK

  ||| Create a valid BarFoo link.
  BarFoo : FooExpr x ELEM
        -> FooExpr y ELEM
        -> {auto prf : ValidBarFoo x y}
        -> FooExpr BarFooTy LINK

  ||| Create a valid BarFoos link.
  BarFoos  : FooExpr x ELEM
         -> DList (FooTy) (\y => FooExpr y ELEM) ys
         -> {auto prf : ValidBarFoos x ys}
         -> FooExpr BarFooTy LINK

-- Local Variables:
-- idris-packages: ("containers")
-- End:
-- --------------------------------------------------------------------- [ EOF ]