I have a rope data type with the invariant that one of its data
constructors can never appear as a leaf.
module Data.Rope where
import Data.Word (Word8)
data Rope = Empty
| Leaf
| Node !Rope !Rope
index :: Rope - Int - Word8
index Empty _ = error empty
index Leaf _
On 10/9/07, Johan Tibell [EMAIL PROTECTED] wrote:
data Rope = Empty
| Leaf
| Node !Rope !Rope
The point is that Empty
can only appear at the top by construction
How about indicating this in your data type? I.e.,
data Rope = Empty | NonEmptyRope
data NonEmptyRope = Leaf
On 10/9/07, David Benbennick [EMAIL PROTECTED] wrote:
On 10/9/07, Johan Tibell [EMAIL PROTECTED] wrote:
data Rope = Empty
| Leaf
| Node !Rope !Rope
The point is that Empty
can only appear at the top by construction
How about indicating this in your data type?
On Tue, 2007-10-09 at 17:40 +0200, Johan Tibell wrote:
On 10/9/07, David Benbennick [EMAIL PROTECTED] wrote:
On 10/9/07, Johan Tibell [EMAIL PROTECTED] wrote:
data Rope = Empty
| Leaf
| Node !Rope !Rope
The point is that Empty
can only appear at the top by
A GADT version seems to generate OK code:
data Top
data NTop
data Rope t where
Empty :: Rope Top
Leaf :: Rope NTop
Node :: !(Rope NTop) - !(Rope NTop) - Rope NTop
index :: Rope t - Int - Word8
index Empty _ = error empty
index Leaf _ = error leaf
index (Node l r) n = index' l n
Johan Tibell wrote:
I have a rope data type [...]
Perhaps you should talk to Derek Elkins about his. It would be nice if
we had fewer, more canonical implementations of popular data structures,
instead of a proliferation of half bakery.
b
