[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Dan Weston]

Dan Weston wrote:
> Brandon S. Allbery KF8NH wrote:
>>
>> On Feb 8, 2008, at 11:14 , Stefan Monnier wrote:
>>
>>>>>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I 
>>>>>> think, the
>>>>>> latter representation should probably be prefered.
>>>>>> (...)
>>> How 'bout treating :+ as similar to `append' rather than similar to 
>>> `cons'?
>>> Basically treat :+ as taking 2 numbers (rather than a number and
>>> a digit).
>>
>> Dumb questions department:  why not define e.g. D'0 .. D'9 as () :* 0 
>> .. () :* 9?  Programmers then get D'1 :* 2, but the library sees () :* 
>> 1 :* 2.
>>
> 
> No, D'0 should be (), not () :* D0. If you allow () :* D0, then you 
> introduce redundant types for the same number:
> 
> In the first case, D'0 :* D'3 == D'3, and D'0 :* D'0 has no instance. In 
> your example, D'3 and D'0 :* D'3 are equivalent, but no longer unify.
> 
> Dan

On second thought, how would you write D'3 :* D0 ? I think maybe using 
the () makes it fundamentally difficult to restrict multiple types for 
the same number.