[Haskell-cafe] Re: What *is* a DSL?

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Tue Oct 27 22:05:33 EDT 2009

On 2009-10-22 14:44, Robert Atkey wrote:
> On Sat, 2009-10-10 at 20:12 +0200, Ben Franksen wrote:
>> Since 'some' is defined recursively, this creates an infinite production for
>> numbers that you can neither print nor otherwise analyse in finite time.
> Yes, sorry, I should have been more careful there. One has to be careful
> to handle EDSLs that have potentially infinite syntax properly.

I find it useful to carefully distinguish between inductive and
coinductive components of the syntax. Consider the following recogniser
combinator language, implemented in Agda, for instance:

  data P : Bool → Set where
    ∅   : P false
    ε   : P true
    tok : Bool → P false
    _∣_ : ∀ {n₁ n₂} → P n₁ →        P n₂  → P (n₁ ∨ n₂)
    _·_ : ∀ {n₁ n₂} → P n₁ → ∞? n₁ (P n₂) → P (n₁ ∧ n₂)

The recognisers are indexed on their nullability; the index is true iff
the recogniser accepts the empty string. The definition of P is
inductive, except that the right argument of the sequencing combinator
(_·_) is allowed to be coinductive when the left argument does not
accept the empty string:

  ∞? : Set → Bool → Set
  ∞? true  A =   A
  ∞? false A = ∞ A

(You can read ∞ A as a suspended computation of type A.) The limitations
imposed upon coinduction in the definition of P ensure that recognition
is decidable. For more details, see


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

More information about the Haskell-Cafe mailing list