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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
