Implementing fixed-sized vectors (using datatype algebra?)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
85 messages Options
12345
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> Nat means "all natural numbers except zero" while Nat0 means "all natural
> numbers (including zero)".  Since in computer science, natural numbers
> usually cover zero, we should use Pos instead of Nat and Nat instead of Nat0.

Sounds sensible, actually Nat and Nat0 is confusing. However I would
rather use Pos and Nat0 to make explicit that naturals include zero .

Depending on the definition of naturals they might or might not
include zero.  http://en.wikipedia.org/wiki/Natural_number

> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the
> latter representation should probably be prefered.  With it, :+ always has a
> number as its left argument and a digit as its right.  Without the () :+ we
> get ugly exceptional cases.
> You can see this, for example, in the instance
> declarations for Compare.  With the second representation, we could reduce
> the number of instances dramatically.  We would define a comparison of digits
> (verbose) and than a comparison of numbers based on the digit comparison (not
> verbose).

Even if () would be preferred from the programmers point of view (I'm
not sure how much we could reduce the number of instances though), it
makes the representation less attractive on the user-side. Anyone
using the library would find it annoying and would wonder why is it
neccessary.

Unless we find a way to use () only internally (we should use a
one-character type to make it shorter to type) I think we should stick
to current representation.

> :+ is already used as the constructor for complex numbers.  We should probably
> use some different operator.

Right. I didn't think about that, thanks.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Dan Weston
I know that naming is arbitrary, but...

Digits in types seems ugly to me. In this case, it is also redundant.
Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem
clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed,
so confusion is even increased with Nat0.

Dan

Alfonso Acosta wrote:

> On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote:
>> Nat means "all natural numbers except zero" while Nat0 means "all natural
>> numbers (including zero)".  Since in computer science, natural numbers
>> usually cover zero, we should use Pos instead of Nat and Nat instead of Nat0.
>
> Sounds sensible, actually Nat and Nat0 is confusing. However I would
> rather use Pos and Nat0 to make explicit that naturals include zero .
>
> Depending on the definition of naturals they might or might not
> include zero.  http://en.wikipedia.org/wiki/Natural_number
>
>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the
>> latter representation should probably be prefered.  With it, :+ always has a
>> number as its left argument and a digit as its right.  Without the () :+ we
>> get ugly exceptional cases.
>> You can see this, for example, in the instance
>> declarations for Compare.  With the second representation, we could reduce
>> the number of instances dramatically.  We would define a comparison of digits
>> (verbose) and than a comparison of numbers based on the digit comparison (not
>> verbose).
>
> Even if () would be preferred from the programmers point of view (I'm
> not sure how much we could reduce the number of instances though), it
> makes the representation less attractive on the user-side. Anyone
> using the library would find it annoying and would wonder why is it
> neccessary.
>
> Unless we find a way to use () only internally (we should use a
> one-character type to make it shorter to type) I think we should stick
> to current representation.
>
>> :+ is already used as the constructor for complex numbers.  We should probably
>> use some different operator.
>
> Right. I didn't think about that, thanks.
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Dan Weston
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
This may be a GHC bug, but even though in the module
Data.TypeLevel.Num.Reps has the header

{-# LANGUAGE EmptyDataDecls, TypeOperators #-}

I still get an error with both ghc and ghci version 6.8.2 unless I throw
in the -XTypeOperators flag.

 > cat Go.hs
import Data.TypeLevel.Num.Reps
main = return (undefined :: D2 :+ D1) >> print "Done"

 > ghc --make Go.hs
[1 of 1] Compiling Main             ( Go.hs, Go.o )

Go.hs:3:31:
     Illegal operator `:+' in type `D2 :+ D1'
       (Use -XTypeOperators to allow operators in types)

 > ghc --make -XTypeOperators Go.hs
[1 of 1] Compiling Main             ( Go.hs, Go.o )
Linking Go ...

 > ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.8.2

Dan

Alfonso Acosta wrote:

> Don't expect anything astonishing yet, but an initial version of the
> library can be found at
>
> http:/code.haskell.org/type-level
>
> To make reviewing easier I have put the haddock-generated documentation at
>
> http://code.haskell.org/~fons/type-level/doc/
>
> Some remarks:
>
> * Only Positive and Natural numerals in decimal representation are
> supported. It would be cool to add support for Integers though.
>
> * The code is based on Oleg's implimentation of type-level binaries
> http://okmij.org/ftp/Computation/resource-aware-prog/BinaryNumber.hs
>
> * exponentiation/log and GCD is not implemented yet
>
> * multiplication is not relational and thus division is broken. I
> tried porting Oleg's multiplication algorithm without success.
>
> * Aliases (in binary, octal decimal and hexadecimal form) for
> type-level values and their value-level reflection functions are
> generated with TH.
>   That implies:
>     * Long compilation time depending on your system
>     * Although errors will always be reported in decimal form, the end
> user can input values using other bases (only for values in the range
> of generated aliases of course)
>
> * It would be cool to have "real" support for other bases apart from decimals
>   * It would imply having unlimited size of input for other bases
> (right now if we want to input a value out of the alises limit,
> decimal reprentation is mandatory)
>   * However, is it feasible? How could it be done without needing to
> implement the operations for each base? WOuld it be possible to
> "overload" the type-level operators so that they worked with different
> representations and mixed representation arguments?
>
> * Booleans are not implemented (Wolfgang?)
>
> I would be happy to hear any suggestions, get code reviews and/or contributions.
>
> Cheers,
>
> Fons
>
>
>
>
>
>
>
>
> On Feb 7, 2008 11:17 AM, Wolfgang Jeltsch <[hidden email]> wrote:
>> Am Donnerstag, 7. Februar 2008 02:47 schrieb Alfonso Acosta:
>>>> The other library I use for type-level programming is HList. It has
>>>> type-level booleans already so you might what to take a look at it if
>>>> you're not already familiar with it.
>>> Thanks I'll have a look at it.
>> I have to admit that I don't like the names HBool, HTrue and HFalse.  What do
>> they mean?  Heterogenous booleans?  Heterogenous truth?  Why it's "Bool"
>> instead of "Boolean" and therefore not conforming to the Prelude convention?
>>
>> Heterogenous lists are not directly about type level computation.  A HList
>> type is usually inhabited.  On the other hand, types which denote type level
>> naturals or type-level booleans are empty data types.  So type level booleans
>> should go into some type level programming library like the one Alfonso and I
>> want to create.  HList should then use these booleans.  This is at least my
>> opinion.
>>
>> Best wishes,
>> Wolfgang
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
On Feb 7, 2008 9:01 PM, Dan Weston <[hidden email]> wrote:
> This may be a GHC bug, but even though in the module
> Data.TypeLevel.Num.Reps has the header
>
> {-# LANGUAGE EmptyDataDecls, TypeOperators #-}
>
> I still get an error with both ghc and ghci version 6.8.2 unless I throw
> in the -XTypeOperators flag.

If you are using type operators in a module you have to supply the
flag, independently of what flags are supplied in other modules.

The same applies for other extensions which modify the _syntax_ of the
language (e.g. Template Haskell etc ...)

So, it's not a bug.

As a side note, even if the TypeOperators flag is supplied GHC 6.8.2
fires an error with the following declaration:

instance (Compare x y CEQ) => x :==: y -- GHC fires a "Malformed
instance header" error

whereas using an equivalent prefix definition works just fine

instance (Compare x y CEQ) => (:==:) x y
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Dan Weston
On Feb 7, 2008 8:38 PM, Dan Weston <[hidden email]> wrote:
> I know that naming is arbitrary, but...
>
> Digits in types seems ugly to me. In this case, it is also redundant.
> Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem
> clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed,
> so confusion is even increased with Nat0.

Ok, fair enough. I changed the names of Positives and Naturals (which
do include 0) for Pos and Nat.

The change (together with a connective rename from :+ to :* ) is
already pushed in the darcs repository.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Richard A. O'Keefe
In reply to this post by Dan Weston

On 8 Feb 2008, at 8:38 am, Dan Weston wrote:

> I know that naming is arbitrary, but...
>
> Digits in types seems ugly to me. In this case, it is also  
> redundant. Everyone but FORTRAN programmers counts from 0, not 1.  
> Nat and Pos seem clear. Nat0 could even mean Nat \ {0}, the  
> opposite of what is proposed, so confusion is even increased with  
> Nat0.

For what it's worth, the Ada names for the types
     {x in Z | x >= 0}
and {x in Z | x > 0}
are "Natural" and "Positive" respectively.  Natural is useful for  
counting stuff;
Positive is useful mainly because Ada practice is to index from 1.
In Z, |N is used for natural numbers, which are defined to include 0.
In modern set theory, both the cardinal and the ordinal numbers start  
with
0, not with 1.

All things considered, I would be very upset indeed if a type called  
"Nat"
or "Natural" or something like that did not include 0.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Wolfgang Jeltsch-2
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie:
> On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> […]

> > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the
> > latter representation should probably be prefered.  With it, :+ always
> > has a number as its left argument and a digit as its right.  Without the
> > () :+ we get ugly exceptional cases.
> > You can see this, for example, in the instance
> > declarations for Compare.  With the second representation, we could
> > reduce the number of instances dramatically.  We would define a
> > comparison of digits (verbose) and than a comparison of numbers based on
> > the digit comparison (not verbose).
>
> Even if () would be preferred from the programmers point of view (I'm
> not sure how much we could reduce the number of instances though), it
> makes the representation less attractive on the user-side. Anyone
> using the library would find it annoying and would wonder why is it
> neccessary.

I wouldn’t wonder.  Leaving out the () :* part just works because our
type-level “values” are not typed, i.e., there aren’t different kinds Digit
and Number but only kind *.  If :+ would be a data constructor (on the value
level), it would take a number and a digit argument which would forbid using
a digit as its left argument.  So I consider using a digit on the left
as “unclean”.  It’s similar to using a number as the second part of a cons
cell in LISP.

> […]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Henning Thielemann

On Fri, 8 Feb 2008, Wolfgang Jeltsch wrote:

> Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie:
> >
> > Even if () would be preferred from the programmers point of view (I'm
> > not sure how much we could reduce the number of instances though), it
> > makes the representation less attractive on the user-side. Anyone
> > using the library would find it annoying and would wonder why is it
> > neccessary.
>
> I wouldn’t wonder.  Leaving out the () :* part just works because our
> type-level “values” are not typed, i.e., there aren’t different kinds Digit
> and Number but only kind *.  If :+ would be a data constructor (on the value
> level), it would take a number and a digit argument which would forbid using
> a digit as its left argument.  So I consider using a digit on the left
> as “unclean”.  It’s similar to using a number as the second part of a cons
> cell in LISP.

seconded
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Implementing fixed-sized vectors (using datatype algebra?)

Stefan Monnier
In reply to this post by Wolfgang Jeltsch-2
>> > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the
>> > latter representation should probably be prefered.  With it, :+ always
>> > has a number as its left argument and a digit as its right.  Without the
>> > () :+ we get ugly exceptional cases.
>> > You can see this, for example, in the instance
>> > declarations for Compare.  With the second representation, we could
>> > reduce the number of instances dramatically.  We would define a
>> > comparison of digits (verbose) and than a comparison of numbers based on
>> > the digit comparison (not verbose).
>>
>> Even if () would be preferred from the programmers point of view (I'm
>> not sure how much we could reduce the number of instances though), it
>> makes the representation less attractive on the user-side. Anyone
>> using the library would find it annoying and would wonder why is it
>> neccessary.

> I wouldn’t wonder.  Leaving out the () :* part just works because our
> type-level “values” are not typed, i.e., there aren’t different kinds Digit
> and Number but only kind *.  If :+ would be a data constructor (on the value
> level), it would take a number and a digit argument which would forbid using
> a digit as its left argument.  So I consider using a digit on the left
> as “unclean”.  It’s similar to using a number as the second part of a cons
> cell in LISP.

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).


        Stefan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Brandon S Allbery KF8NH

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.

--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [hidden email]
system administrator [openafs,heimdal,too many hats] [hidden email]
electrical and computer engineering, carnegie mellon university    KF8NH


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Henning Thielemann

On Fri, 8 Feb 2008, 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.

Do you remember that they talk about types D0, D1, and so on?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Dan Weston
In reply to this post by Brandon S Allbery KF8NH
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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Implementing fixed-sized vectors (using datatype algebra?)

Aaron Denney
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
On 2008-02-05, Alfonso Acosta <[hidden email]> wrote:

> On Feb 5, 2008 4:10 PM, Henning Thielemann
><[hidden email]> wrote:
>>
>> On Fri, 1 Feb 2008, Aaron Denney wrote:
>>
>> > On 2008-02-01, Bjorn Buckwalter <[hidden email]> wrote:
>> > > If Naturals had been sufficient for me I wouldn't have done my own
>> > > implementation (I'm unaware of any other implementation of Integers).
>> > > And there is certainly a lot of value to the clearer error messages
>> > > from a decimal representation.
>> >
>> > I did a balanced-base-three (digits are 0, and +- 1) representation to
>> > get negative "decimals".
>>
>> Nice. In German the digit values are sometimes called "eins, keins, meins". :-)
>
> I'm almost done with the decimal library but it would be nice to check
> some Integer implementations for future inclusion. So, Aaron, Björn,
> are your implementations available somewhere?

http://ofb.net/~wnoise/repos/dimensional/

--
Aaron Denney
-><-

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bjorn Buckwalter-2
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
On Feb 6, 2008 8:47 PM, Alfonso Acosta <[hidden email]> wrote:

> On Feb 7, 2008 2:30 AM, Bjorn Buckwalter <[hidden email]> wrote:
> > Ok. Is this what people want -- one big hold-all library with
> > everything, as opposed to smaller more specialized packages? I guess I
> > can see advantages (real or perceived) to both approaches.
>
> Apart from Dockins' typenats library there are no other user-friendly
> specific type-level libraries that know, so I cannot really tell if
> people would prefer a hold-all library or a couple of more granular
> specialized ones.
>
> Right now is not hold-all at all (it is still vaporware actually :)),
> so I think there's no reason to discuss that at this point. Let's see
> what people think.

Right, of course. I'll be taking a look at your no-longer-vaporware! ;)
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Wolfgang Jeltsch-2
In reply to this post by Stefan Monnier
Am Freitag, 8. Februar 2008 17:14 schrieb Stefan Monnier:

> >> > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think,
> >> > the latter representation should probably be prefered.  With it, :+
> >> > always has a number as its left argument and a digit as its right.
> >> > Without the () :+ we get ugly exceptional cases.
> >> > You can see this, for example, in the instance
> >> > declarations for Compare.  With the second representation, we could
> >> > reduce the number of instances dramatically.  We would define a
> >> > comparison of digits (verbose) and than a comparison of numbers based
> >> > on the digit comparison (not verbose).
> >>
> >> Even if () would be preferred from the programmers point of view (I'm
> >> not sure how much we could reduce the number of instances though), it
> >> makes the representation less attractive on the user-side. Anyone
> >> using the library would find it annoying and would wonder why is it
> >> neccessary.
> >
> > I wouldn’t wonder.  Leaving out the () :* part just works because our
> > type-level “values” are not typed, i.e., there aren’t different kinds
> > Digit and Number but only kind *.  If :+ would be a data constructor (on
> > the value level), it would take a number and a digit argument which would
> > forbid using a digit as its left argument.  So I consider using a digit
> > on the left as “unclean”.  It’s similar to using a number as the second
> > part of a cons cell in LISP.
>
> 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).

So what would (D1 :* D1) :* (D2 :* D2) mean then?

>         Stefan

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Wolfgang Jeltsch-2
On Feb 8, 2008 4:10 PM, Wolfgang Jeltsch <[hidden email]> wrote:

> Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie:
> > Even if () would be preferred from the programmers point of view (I'm
> > not sure how much we could reduce the number of instances though), it
> > makes the representation less attractive on the user-side. Anyone
> > using the library would find it annoying and would wonder why is it
> > neccessary.
>
> I wouldn't wonder.  Leaving out the () :* part just works because our
> type-level "values" are not typed, i.e., there aren't different kinds Digit
> and Number but only kind *.  If :+ would be a data constructor (on the value
> level), it would take a number and a digit argument which would forbid using
> a digit as its left argument.

Well, the fact is that :+ (or :* as it is called now) is not a value
constructor but a type constructor as you said, so I don't think your
example really applies here. Besides, you should be regarded :* as (,)
and not as a constructor which "would take a number and a digit
argument which would forbid using a digit as its left argument."
Indeed, :* exists as a value-level constructor too and works exactly
like that.

Furthermore, you probably consider using () as natural and logical
because you are still thinking from the implementation side. If you
forget the implementation details and think as a user who barely wants
to write type-level numerical literals, :* is simply an ugly syntactic
requirement which we cannot get rid of (I would be happy to find
another representation closer to a literal, but I couldn't until now).
That is not the case for (), since, as shown in the initial
implementation, can be avoided.

So, for me, it's just a matter of usability and syntax, the closer the
representation can be to literals, the better. I don't see the
semantic implications of :* as a valid argument. For me, :* is just an
unavoidable ugly syntactical token without meaning. Imagine that for
some reason, adding () as a prefix in every numerical literal made the
implementation of a compiler slightly easier/faster. I bet users would
rant about it till exhaustion :)

If the argument was that,  for some reason, () was proven to speed up
the implementation or make a big maintainability difference (I still
have my doubts) it would maybe make more sense (I still wouldn't be
sure if it pays off though). Maybe it would be a good idea to create a
patch and see what happens :)

As a side note, I think that type-value digits actually are "typed"
(metatyped maybe is a nicer term?). Class constraints take the role of
types in this case.

After all (sorry if the definition is imprecise), a type establishes a
set of valid values. "Nat n => n" does exactly that. For example, it
forces type-level naturals to be normalized (i.e. numerals with
leading zeros don't satisfy the Nat constraint)


> So I consider using a digit on the left
> as "unclean".  It's similar to using a number as the second part of a cons
> cell in LISP.

Again, the comparisson is based on semantical implications of the
implementation which shouldn't be visible for, or at least not taken
into consideration by,  the final user.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Stefan Monnier
On Feb 8, 2008 5:14 PM, Stefan Monnier <[hidden email]> wrote:
> 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).


Interpreting it like that would certainly make make more sense. But
again, I think that :* should be interpreted just as an unavoidable
syntactical annoyance without meaning or interpretation.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Wolfgang Jeltsch-2
On Feb 9, 2008 4:08 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> So what would (D1 :* D1) :* (D2 :* D2) mean then?

Nothing. That value doesn't satisfy the Nat or Post class constraints
and should be taken into consideration.

Why should :* be provided a meaning? it is an unavoidable syntactical
connective for all that I care. The meaning is provided by class
constraints and that's all that matter from the semantical point of
view.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
On Feb 9, 2008 11:33 PM, Alfonso Acosta <[hidden email]> wrote:
> On Feb 8, 2008 4:10 PM, Wolfgang Jeltsch <[hidden email]> wrote:

> example really applies here. Besides, you should be regarded :* as (,)
> and not as a constructor which "would take a number and a digit

Sorry for my lousy English, I meant "you should regard" not "you
should be regarded".
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12345