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

[Nils Anders Danielsson]

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
http://www.cs.nott.ac.uk/~nad/listings/parser-combinators/TotalRecognisers.html.

--
/NAD



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.