Embedded Domain Specific Type Systems for Declarative EDSls

Posted on July 4, 2015

Categories: idris

Example of Embedded Domain Specific Type Systems for Declarative EDSLs. The full code can be found: https://gist.github.com/jfdm/2c37389f89203448f763

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.

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

The type 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.