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.