On Jan 31, 2008 3:03 PM, Wolfgang Jeltsch wrote:

Hello Fons,

interestingly, it occured to me yesterday that the graphics part of Grapefruit would benefit from fixed sized vectors. I think we should implement some small Cabal package which just provides this and upload it to the HackageDB. Are you interested in cooperating with me on this?

Sure I am! Actually, thanks to the pointers provided by Henning I learned that Oleg (who else!) already has implemented them. See http://okmij.org/ftp/Haskell/number-parameterized-types.html http://www.haskell.org/tmrwiki/NumberParamTypes http://okmij.org/ftp/Haskell/number-param-vector-code.tar.gz (Oleg's multiple flavour implementations of fixed-sized vectors) I think we should base our implementation on Oleg's (for which we need his permission). Actually, I think we should create two separate libraries. One for decimal type-level arithmetic and another for the vector implementation itself. What do you think?

Hello Henning, Thursday, January 31, 2008, 5:49:23 PM, you wrote:

I remember that type-level arithmetic is already implemented somewhere, certainly more than once, but certainly seldom in a nicely packaged form.

one more: darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

I remember that type-level arithmetic is already implemented somewhere, certainly more than once, but certainly seldom in a nicely packaged form.

erm, here http://www.haskell.org/haskellwiki/Type_arithmetic

Yep, there seem to be a few implementations around (decimal, binary, peano) but Oleg's decimal one is likely to be the most friendly when it comes to compiler errors etc ..

http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Fixed.html#t...

also here: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numbers-2007.9.25 ?

I'm probably missing something, but I don't understand how these libraries could help. Thanks, Fons

Wolfgang Jeltsch wrote:

Well, the representation (D1,D2,D9) might be considered more readable. It has the disadvantage of a fixed maximum size for the numbers. Which takes me to a point I had already considered some time ago: Wouldn’t it be good if we had just a type

data Pair val1 val2 = Pair val1 val2

and if then (val1,val2,…,valn) would just be syntactic sugar for this:

val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…))

I've thought of that too.. besides the asymmetry, the presence of _|_/seq makes them actually not equivalent though, unfortunately ~Isaac

Wolfgang Jeltsch wrote:

Am Freitag, 1. Februar 2008 05:11 schrieben Sie:

...

Wolfgang Jeltsch wrote:

...

Well, the representation (D1,D2,D9) might be considered more readable. It has the disadvantage of a fixed maximum size for the numbers. Which takes me to a point I had already considered some time ago: Wouldn’t it be good if we had just a type

data Pair val1 val2 = Pair val1 val2

and if then (val1,val2,…,valn) would just be syntactic sugar for this:

val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…)) I've thought of that too.. besides the asymmetry, the presence of _|_/seq makes them actually not equivalent though, unfortunately

~Isaac

With Ryan’s proposal (using strictness annotations) the new representation should be equivalent to the old one. Or am I missing something?

adding the strictness annotation seems to make them equivalent, yes I agree (I hadn't seen that post when I wrote that reply) ~Isaac

What about FixedVector for the vector library and DecTypArith (maybe too long) or DecTypes for the type-level decimal arithmetic library?

Actually it would maybe be better to create common high-level interface that could include unary, binary and decimal arithmetic so that the library could be easily reused in other projects (people like Bjorn, seem to be using the unary implementation). I don't know if it would be feasible though.

On 2008-02-01, Bjorn Buckwalter 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". Again, for a proof-of-concept dimensional analysis arithmetic. No problem with the stack, but the error messages are still less than clear. -- Aaron Denney -><-

On Feb 5, 2008 4:10 PM, Henning Thielemann wrote:

On Fri, 1 Feb 2008, Aaron Denney wrote:

...

On 2008-02-01, Bjorn Buckwalter 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?

On Feb 5, 2008 8:29 PM, Bjorn Buckwalter wrote:

On Feb 5, 2008 2:16 PM, Alfonso Acosta wrote:

...

On Feb 5, 2008 4:10 PM, Henning Thielemann wrote:

...

On Fri, 1 Feb 2008, Aaron Denney wrote:

...

On 2008-02-01, Bjorn Buckwalter 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?

As noted elsewhere in the thread my implementation is available at:

http://www.buckwalter.se/~bjorn/darcs/dimensional/Numeric/NumType.lhs

Thanks!

It is my intent to extract this (self-contained) module to its own package and put on hackage. It's been a low priority for me but I'm rather incentivized by this thread.

Great! How about joining efforts? As I said I almost have a preliminary version of the decimal library which I'll realease for reviewing purpouses soon (It won't include Integer computations though)

On Feb 6, 2008 4:32 AM, Bjorn Buckwalter wrote:

Well, could you elaborate a little on joining efforts? The effort I was planning to invest in my package consists mainly of creating a .cabal file plus some logistics to get tarballs to where they have to be.

I understand that you (and Wolfgang) are creating a library of type level decimals for the purpose of constraining vector (list?) lengths. After that I haven't been paying attention fully to the thread. Is the goal to create a general-purpose library for type-level programming and my module would fit into that grander scheme?

Yes,the idea is to create a Cabal-ready wide-scope type-level programming library, joining the operations implemented in the different type-level libraries which are around. The goal (or at least mine) is to provide a common reusable type-level library which saves constantly reinventing the wheel. I'll provide an initial implementation (just including naturals in decimal representation) soon. Wolfgang suggested adding booleans at a later point too if I recall properly. Any useful type-level operation should have a place in the library.

Or did you have something else in mind with joining efforts? E.g. help reviewing your code or writing new code?

This would certainly help too.

On Feb 7, 2008 2:30 AM, Bjorn Buckwalter 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.

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.

In fact, if you are serious about creating the de facto(?) type-level programming library trying to get Oleg involved would be very beneficial both in terms of innovation and credibility.

Sure. I've actually been exchanging mail with Oleg. He has given me some useful suggestions and contributed with some code. He didn't mention to what point he wanted to get involved though, but I'm sure he will try to help.

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

On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch 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.

On Feb 7, 2008 8:38 PM, 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.

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.

Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie:

On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch 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

...

...

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

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?

Am Sonntag, 10. Februar 2008 05:14 schrieben Sie:

[…]

Now some functions which I wasn't able to define

Concat function. This would be the naive implementation, but it fails to compile.

(<+>) :: Add s1 s2 s3 => FSVec s1 a -> FSVec s2 a -> FSVec s3 a NullV <+> ys = ys (x:>xs) <+> ys = x :> (xs <+> ys)

Hmm, we would have to find a way to implement lemmas. In this case, the lemma that succ (x + y) = succ x + y. At the moment, I’ve no good idea how to do that.

Tail function, which is also incorrect.

tailV :: Succ s' s => FSVec s a -> FSVec s' a tailV (x :> xs) = xs

Maybe this problem is similar to the one I came across earlier. See my mail on http://www.haskell.org/pipermail/haskell/2007-September/019757.html and the replies to it.

And finally, vector, which is supposed to build a fixed-sized vector out of a list.

The ideal type for the function would be:

vector :: [a] -> FSVec s a

But there is no apparent way in which to obtain s based on the length of the input list.

[1] shows a way in which to create vector using CPS style and a reification function:

reifyInt :: Int -> (forall s . Nat s => FSVect s a -> w) -> w

The result would be a function with the following type:

vector :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w

Nevertheless, I'm not fully satisfied by it.

I suppose, it’s the best we can get without having dependent types. Others might correct me.

[…]

Some remark concerning spelling: Would it be possible to drop the V at the end of the function names? I think the fact that those functions are about “vectors” is better expressed by qualification: import Data.List as List import Data.TypeLevel.Vector as Vector -- Usage: Vector.last, List.last, … Compare this to the functions in Data.Map, Data.Set, etc. They also use insert, etc. instead of insertM, insertS, etc. Note that the latter would quickly lead to ambiguities because insertM would stand for map insertion as well as for multiset insertion. Similar with sets and sequences. Best wishes, Wolfgang

Hi Dan, On Feb 10, 2008 6:08 PM, Dan Licata wrote:

...

...

The ideal type for the function would be:

vector :: [a] -> FSVec s a

Well, I probably didn't express myself properly when writing "The ideal type", "the first type which comes to mind" would have been more accurate. Thanks for your explanation, which is actually much better than mine and, in fact, almost identical to the one included in http://ofb.net/~frederik/vectro/draft-r2.pdf

Am Montag, 11. Februar 2008 18:17 schrieben Sie:

[…]

As suggested by the pointer you provided, I redefined FSVec and tailV using a transformating of Succ into a type synonym family (see the end of this mail for its full definition) but it didn't help.

Be careful! Type family support is still broken in GHC 6.8. And the whole type system machinery seemed to be rather broken when I last checked a then current development version (6.9).

data FSVec :: * -> * -> * where NullV :: FSVec D0 a (:>) :: FSVec s a -> FSVec (Succ s) a

tailV :: FSVec s a -> FSVec (Succ s) a tailV (x :> xs) = xs

tailV leads to this error (which I don't really understand :S)

GADT pattern match in non-rigid context for `:>' Tell GHC HQ if you'd like this to unify the context In the pattern: x :> xs In the definition of `tailV': tailV (x :> xs) = xs

I think, this can be solved with a type declaration. At least I heard about something like this. Probably googling for this error message will help.

My first impressions about using type synonym families (as opposed to multiparameter type classes) to fake dependent types are:

[…]

I think, type synonym families are not a replacement for multiparameter classes but for functional dependencies. So you will still need multiparameter classes in certain places but you’ll be able to get rid of functional dependencies (except for certain cases where fundeps are combined with overlapping instances, at least).

- I'm maybe missing something, but it seems that type synonym families don't work nicely with typeclass constraints.

this is ilegal (syntax error):

type family Nat x => Succ x :: *

this is ilegal too (another syntax error):

type instance Nat x => Succ (x :* D0) = x :* D1

Maybe you should put your type family synonym into a class where it becomes an associated type synonym: class Nat x where type Succ x :: * […]

and finally I was really surprised to know that, using the type synonym family this is illegal too!

toInt (succRef d0)

the expression above leads to the following error:

No instance for (Data.TypeLevel.Num.Sets.NatI (Succ D0))

But .... Succ D0 = D1, and D1 and D1 _is_ an instance of NatI !

Maybe a bug. As I said, you cannot expect type families to work reliably at the moment.

[…]

...

Some remark concerning spelling: Would it be possible to drop the V at the end of the function names? I think the fact that those functions are about "vectors" is better expressed by qualification:

Right, do you think the same should be done for Data.TypeLeve.Num.Ops ? (succRef, predRef, addRef, subRef and friends ...)

Yes, I think so.

Best Regards,

A really frustrated Fons

:-( Best wishes, Wolfgang

[…]

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

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

Am Samstag, 9. Februar 2008 23:46 schrieben Sie:

On Feb 9, 2008 4:08 PM, Wolfgang Jeltsch 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.

I was just refering to Stefan’s argument that :* should be treated as a form of concatenation. From your point of view, it’s clear, of course. Best wishes, Wolfgang

On Feb 8, 2008 4:10 PM, 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.

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.

Am Samstag, 9. Februar 2008 23:33 schrieben Sie:

On Feb 8, 2008 4:10 PM, 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.

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.

My arguments were not so much about implementation, I think. I’d see a type-level number as a list of digits, and a list has the form x1 : (x2 : (… : (xn : [])…)) or ((…([] `Snoc` x1) `Snoc` …) `Snoc` x(n-1)) `Snoc` xn. From this point of view, it’s reasonable to have the extra () :*. On the other hand, it might be sensible to give the user the illusion that :* is part of a special syntax while it’s actually an operator. I’m not really sure what the better approach is. Best wishes, Wolfgang

On Feb 7, 2008 9:01 PM, Dan Weston 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

On 2008-02-05, Alfonso Acosta wrote:

On Feb 5, 2008 4:10 PM, Henning Thielemann wrote:

...

On Fri, 1 Feb 2008, Aaron Denney wrote:

...

On 2008-02-01, Bjorn Buckwalter 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 -><-

On Feb 1, 2008 10:33 PM, Wolfgang Jeltsch wrote:

...

Actually it would maybe be better to create common high-level interface that could include unary, binary and decimal arithmetic so that the library could be easily reused in other projects (people like Bjorn, seem to be using the unary implementation). I don't know if it would be feasible though.

I'd say, let's start with the decimal thing. We can extend our package later if there's a need to do this, can't we?

OK, let's do it like that.

On Feb 1, 2008 10:32 PM, Wolfgang Jeltsch wrote:

Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta:

...

On Jan 31, 2008 11:35 PM, Wolfgang Jeltsch

...

This is essentially what I had in mind. While Oleg's implementation needs a "thrusted core", the GADT solution doesn't.

True. However using GADTs doesn't allow to internally make use of Arrays, which (tell me if I'm wrong) are likely to be faster than the naive GADT implementation.

It depends. My first GADT implementation is equivalent to the [] type and often [] is better than arrays. For example, if you read the contents of a file and process it with maps, filters, etc., [] is likely to give you constant space usage which arrays don't. If you want to lookup elements by index, then arrays are better, of course. For my purpose, it would be fine to use a []-like implementation, I think.

For mine it would be fine too. Let's implement our needs and then maybe extend it if someone rants about it.

...

To make it friendlier for the end user I thought about defining aliases for lets say the first 10000 numbers using Template Haskell. That could even make error reports friendlier (not sure to what point though). What do you think?

I have no clear opinion about that at the moment. Maybe it's okay to use the representation directly. This way, we don't introduce a dependeny on the Template Haskell language extension (which is only supported by GHC), and the actual representation will occur in error messages anyway whenever the message shows a computed number.

Well, my EDSL already makes extensive use of TH. So, being selfish, it wouldn't be a problem for me (or any other GHC user) and I think it would make the library much more usable. Just compare f :: List (() :- D1 :- D0 :- D0 :- 1000) Int -> List (() :- D1 :- D0 :- D0 :- D0) Int with, let's say f :: List A1000 Int -> List A1000 Int Again, if someone complains about the TH dependency, the aliases could be generated by TH but saved statically in a module for each release.

...

So, we'll be making two separate libraries then. We should think about names.

What about FixedVector for the vector library and DecTypArith (maybe too long) or DecTypes for the type-level decimal arithmetic library?

Alas, there is an inconsistency in naming packages already. Some prefer names which are entirely lowercase, some prefer camel case. I prefer lowercase, with hyphens separating parts of the name. And I also don't like unusual abbreviations like "typ" (not much shorter than "type"). To mention arithmetics is not so important. So maybe something like "type-level-decimals"?

Maybe it's better to put different type-level programming things into a single package. Then we could name this package "type-level" or something similar. We could start with our decimals. Other type-level things could be added later. I already have some code about type-level booleans. It's not very sensible to put these few lines into a separate package. It might be nice if we had a general type-level programming package where I could put this code into.

Sounds sensible. However, I would rather prefer something like type-level-comp (from type level computations) or type-level-prog (from type level programming). Type level by itself doesn't describe the functionality of the package.

As for the name of the fixed-size list package, I have to say that I don't like the term "vector" in this context. A vector is actually something with addition and scalar multiplication defined on it. Maybe we should make also this package's scope wider. What about something like "safe-data" or similar?

I think safe-data is a bit too general and might lead to confusion with other safe data packages (namely Mitchell's Safe library). Since the main particularity of the library is that safety properties are achieved via "emulating" dependent types I think that light-dependent-types (from lightweight dependent types), number-parameterized-data or simply parameterized-data (this is the name I like best) would be more appropiate.

Am Samstag, 2. Februar 2008 14:54 schrieben Sie:

On Feb 1, 2008 10:32 PM, Wolfgang Jeltsch wrote:

...

Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta: […]

...

...

To make it friendlier for the end user I thought about defining aliases for lets say the first 10000 numbers using Template Haskell. That could even make error reports friendlier (not sure to what point though). What do you think?

I have no clear opinion about that at the moment. Maybe it's okay to use the representation directly. This way, we don't introduce a dependeny on the Template Haskell language extension (which is only supported by GHC), and the actual representation will occur in error messages anyway whenever the message shows a computed number.

Well, my EDSL already makes extensive use of TH. So, being selfish, it wouldn't be a problem for me (or any other GHC user) and I think it would make the library much more usable.

Just compare

f :: List (() :- D1 :- D0 :- D0 :- 1000) Int -> List (() :- D1 :- D0 :- D0 :- D0) Int

with, let's say

f :: List A1000 Int -> List A1000 Int

Again, if someone complains about the TH dependency, the aliases could be generated by TH but saved statically in a module for each release.

Hmm, this could be a compromise although I’m not sure whether it is sensible to have a module with thousands of declarations. Another solution would be to put the Template Haskell convenience stuff into a separate package. The core package would probably be usable with Hugs too, while the convenience package would be usable only with GHC. At the moment, I’m not sure how often I’ll need to state type-level numbers explicitely. So currently I cannot know how important aliases for type-level numbers are.

...

...

So, we'll be making two separate libraries then. We should think about names.

What about FixedVector for the vector library and DecTypArith (maybe too long) or DecTypes for the type-level decimal arithmetic library?

Alas, there is an inconsistency in naming packages already. Some prefer names which are entirely lowercase, some prefer camel case. I prefer lowercase, with hyphens separating parts of the name. And I also don't like unusual abbreviations like "typ" (not much shorter than "type"). To mention arithmetics is not so important. So maybe something like "type-level-decimals"?

Maybe it's better to put different type-level programming things into a single package. Then we could name this package "type-level" or something similar. We could start with our decimals. Other type-level things could be added later. I already have some code about type-level booleans. It's not very sensible to put these few lines into a separate package. It might be nice if we had a general type-level programming package where I could put this code into.

Sounds sensible. However, I would rather prefer something like type-level-comp (from type level computations) or type-level-prog (from type level programming). Type level by itself doesn't describe the functionality of the package.

Hmm, package names don’t have to be descriptive. Short names tend to sound better and be easier to remember. My FRP GUI and graphics library is named Grapefruit. This name makes hardly any sense. It refers to the previous library Fruit and the fact that I like Grapefruits—nothing more. But it’s a name, people can remember more easily than FRGGLER (Functional Reactive GUI and Graphics Library with Extensible Records). ;-) In addition, abbreviations like “comp” typically have the problem of being ambiguous: computation, composition, component, … So I still prefer type-level.

...

As for the name of the fixed-size list package, I have to say that I don't like the term "vector" in this context. A vector is actually something with addition and scalar multiplication defined on it. Maybe we should make also this package's scope wider. What about something like "safe-data" or similar?

I think safe-data is a bit too general and might lead to confusion with other safe data packages (namely Mitchell's Safe library). Since the main particularity of the library is that safety properties are achieved via "emulating" dependent types I think that light-dependent-types (from lightweight dependent types), number-parameterized-data or simply parameterized-data (this is the name I like best) would be more appropiate.

parametrized-data looks good. The others seem to be too long again. So type-level + parametrized-data is my vote. But don’t let’s spend too much time discussing the name. ;-) Best wishes, Wolfgang

Am Montag, 4. Februar 2008 13:22 schrieben Sie:

On Feb 4, 2008 12:36 PM, Wolfgang Jeltsch wrote: […]

I don't still know how many people would be interested in using the type-level library so, again, I think it won't hurt to include the TH-generated aliases and then change it if some non-GHC user rants about it.

Okay, let’s do so for now.

...

So type-level + parametrized-data is my vote. But don't let's spend too much time discussing the name. ;-)

Fair enough. type-level + parameterized-data it is then (unless someone else has a better suggestion). I'm going to begin coding now.

Yes, go ahead. :-) Thanks a lot.

I'll host the project in community.haskell.org, do you have an account there?

Now, I haven’t. :-(

PS: BTW, I asked Oleg for permission and, as expected, agreed to create the library under a BS-D license.

Great. So the packages you create now will be released under BSD3, right? Best wishes, Wolfgang

Am Montag, 4. Februar 2008 20:44 schrieben Sie:

...

...

I'll host the project in community.haskell.org, do you have an account there?

Now, I haven't. :-(

Well, you can request one at http://community.haskell.org/admin/account_request.html if you want

Otherwise I'll take the maintainer role.

I’m fine with you having the maintainer role as long as you accept a patch from me from time to time. :-) Best wishes, Wolfgang

Am Montag, 11. Februar 2008 21:44 schrieben Sie:

Alfonso Acosta wrote:

...

...

So type-level + parametrized-data is my vote. But don't let's spend too much time discussing the name. ;-)

Fair enough. type-level + parameterized-data it is then (unless someone else has a better suggestion). I'm going to begin coding now.

hang on, "parametrized" or "parameterized"? -- both seem like plausible spellings, but there's an "e" different between what you two said!

What spelling is more common? Best wishes, Wolfgang

Richard A. O'Keefe wrote:

Concerning "parametrized" vs "parameterized" On 12 Feb 2008, at 11:21 pm, Wolfgang Jeltsch asked:

...

What spelling is more common?

Strictly speaking, there is no such word in English as "parametrized".

Except that, strictly speaking, there *is* a word "parametrized" in English. I have read and heard it from many (at least 10) independent uses by educated native writers of English. I use it myself. Merriam-Webster agrees with me [1]. The OED editorial board is no Académie Anglaise: its criterion is descriptive, not prescriptive, by its own admission [2]. Whether a spelling is accepted by the OED has nothing to do with morphological rules (or "proper" usage) and everything to do with established usage. That is why we say "impulse" but not "compulse", the antonym of "increment" is not "excrement", we have "electrify/liquify" but "electrification/liquefaction", "duh" and "no duh" are near-synonyms, etc. To directly answer Wolfgang's question: "parameterized" is the more common. It is "more correct" only insofar as it is the more common. [1] http://www.merriam-webster.com/dictionary/parametrized Main Entry: pa·ram·e·ter·ize Pronunciation: \p?-?ra-m?-t?-?ri-z, -m?-?tri-z\ Variant(s): or pa·ram·e·trize \-?ra-m?-?tri-z\ Function: transitive verb Inflected Form(s): pa·ram·e·ter·ized or pa·ram·e·trized; pa·ram·e·ter·iz·ing or pa·ram·e·triz·ing Date: 1940 : to express in terms of parameters [2] http://www.oed.com/about/writing/choosing.html "...a new word is not included in the OED unless it has "caught on" and become established in the language. Words that are only used for a short period of time, or by a very small number of people, are not included." Dan Richard A. O'Keefe wrote:

Concerning "parametrized" vs "parameterized" On 12 Feb 2008, at 11:21 pm, Wolfgang Jeltsch asked:

...

What spelling is more common?

Strictly speaking, there is no such word in English as "parametrized". There is no general morphological rule "Xer => Xrized" in English. The only spelling accepted by the OED is "parameterized", which annoys me because I prefer the -ise- spelling.

Amusingly, one of the quotations in the www.oed.com entry for "parameterized" actually spells it "parametrized"; I don't know whether the source had it that way or whether the data entry error was at the OED.

On Feb 14, 2008 10:40 AM, Wolfgang Jeltsch wrote:

So we should "parameterized" for the package name.

That's the packagename I've been using. I'm done with a basic implementation but I'd like to test some other things before showing the code. On the other hand, I think that the type-level library is almost ready for it's initial release. Before uploading it to Hackage and making an announcement I would be pleased to receive some comments/suggestions. Here is the darcs repository: http://code.haskell.org/type-level/ Here is the haddock-generated documentation: http://code.haskell.org/~fons/type-level/doc/ There are still some things missing which would be cool to have: * Native support of representations in different bases (I don't know if it's feasible) * Support of negative integers (Björn?) * Support of type-level Booleans (Wolfgang?)

2008/2/19 Wolfgang Jeltsch :

Attached is just a quickly hacked Boolean module. Nothing very special. I'd be happy if you could prettify this (choose better names, add documentation, etc.). Thanks for any effort.

Thanks to you for the module. I have a few questions though. Why are the value-level reflecting functionsimplemented as type-class methods? It makes the code more verbose and I don't see any advantage compared to simply defining a function per class. Let me show you an example: This is your implementation of Not: class (Boolean boolean, Boolean boolean') => Not boolean boolean' | boolean -> boolean', boolean' -> boolean where not :: boolean -> boolean' instance Not False True where not _ = true instance Not True False where not _ = false This is how I would do it: class (Boolean boolean, Boolean boolean') => Not boolean boolean' | boolean -> boolean', boolean' -> boolean where instance Not False True instance Not True False not :: Not a b => a -> b not = undefined Furthermore, why did you choose to use Boolean instead of simply Bool? Cheers, Fons

OK I'll include the module after I change the things mentioned. BTW, I finally have an initial version of the parameterized-data package: Darcs repository: http://code.haskell.org/parameterized-data Haddock documentation: http://code.haskell.org/~fons/parameterized-data/doc/ Any comments/suggestions would be appreciated. To fix the problem of the "vector" constructor I included a Template Haskell variant. It is quite simple to use: $ ghci -XTemplateHaskell Prelude> :m +Data.Param Prelude Data.Param> $(vectorTH [1 :: Int, 2, 3, 4]) Prelude Data.Param> :t $(vectorTH [1 :: Int, 2, 3, 4]) (vectorTH [1 :: Int, 2, 3, 4]) :: (Num t) => FSVec Data.TypeLevel.Num.Reps.D4 t Note that the size parameter (type-level decimal numeral) is correct. It would be nice to be able to use a Quasiquoter [1] (available in GHC HEAD) to enable pattern matching and custom syntax to Vector literals. However, I was bitten by a polymorphism problem when implementing it: see [2] for details [1] http://www.haskell.org/ghc/dist/current/docs/users_guide/template-haskell.ht... [2] http://www.haskell.org/pipermail/template-haskell/2008-February/000655.html On Wed, Feb 20, 2008 at 2:26 AM, Wolfgang Jeltsch wrote:

Am Mittwoch, 20. Februar 2008 00:39 schrieben Sie:

...

Why are the value-level reflecting functionsimplemented as type-class methods? It makes the code more verbose and I don't see any advantage compared to simply defining a function per class. Let me show you an example:

This is your implementation of Not:

class (Boolean boolean, Boolean boolean') => Not boolean boolean' | boolean -> boolean', boolean' -> boolean where not :: boolean -> boolean'

instance Not False True where not _ = true

instance Not True False where not _ = false

This is how I would do it:

class (Boolean boolean, Boolean boolean') => Not boolean boolean' | boolean -> boolean', boolean' -> boolean where

instance Not False True instance Not True False

not :: Not a b => a -> b not = undefined

Your definition of the not function uses the implementation detail that false and true are actually undefined. My implementation of the not function also works if false and true are defined to be something different. Of course, false and true are in the same library, so we know this implementation detail and could make use of it.

...

Furthermore, why did you choose to use Boolean instead of simply Bool?

To avoid a name clash. Feel free to change this.

Note that False and True don't cause a name clash since they live in a namespace different from the one Prelude's False and True live in.

...

Cheers,

Fons

Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Feb 20, 2008 at 11:26 AM, Wolfgang Jeltsch wrote:

Hello Fons,

why do you use the term vector? I'd say that this term is more or less wrong for what this type is about. The distinguishing property of vectors compared to lists is that there is addition and scalar multiplication for vectors.

That depends on how you interpret the word vector, which is polysemous: http://en.wikipedia.org/wiki/Vector You are interpreting it as "An element in a vector space, often represented as a coordinate vector" whereas in this case I try to mean "A one-dimensional array".

The data type you defined is a fixed size list.

The fact that FSVec is internally implemented using lists doesn't imply that FSVec should be interpreted as a list. FSVec is an ADT and I could as well have used something else to implement it (inmutable arrays for instance).

On Fri, Mar 14, 2008 at 5:30 PM, Wolfgang Jeltsch wrote:

I have a feedback from my Grapefruit co-developer about those aliases in the type-level package. He told me that on his machine, building this package took about 15 minutes, obviously because the machine ran out of RAM. He also told me that the generated object code was very large, and that loading the documentation page generated by Haddock took very long.

Fair point, it akes quite some time in my machine too (not 15minutes though)

And he made a very good point: Who needs aliases for *all* numbers until, say, 10000? Who needs to hard-code the vector length 8247 in his code?

If I remember correctly aliases are generated until decimal 5000, which might me really long anyway.

I think that in practice, you only need very few numbers hard-coded. So it might be better to export a function for letting the package user generate the necessary aliases himself.

I even think that it is probably sensible to drop the alias thing completely, at least if you have vector lengths in mind. What vector lengths will appear as fixed in a real world program? 1000? I think, usually you have only sizes like 2 or 3 hard-coded, for vectors in the mathematical sense. And their representation is already very short: D2, D3, … Remember that computed numbers are not shown as aliases in error messages, only numbers that directly appear in your code.

My co-author also mentioned that he doesn't see much use for octal and hexadecimal notation.

So I propose to drop alias support from type-level or at least let the package user do the necessary generation.

I think that removing aliases completely is not a good idea. How about generating much lower aliases for decimals (lets say until 1000), droping the other bases, and exporting a function to extended the alias range at will? (that function could perfectly include the other bases as well). Something called extendAliases would do. I don't have the time to work on it now, but if you send me a patch I'd be happy to apply it. It should be something simple to do. All the Template Haskell machinery is already coded.

...

[…]

Best wishes, Wolfgang

On Fri, Mar 14, 2008 at 9:58 PM, Wolfgang Jeltsch wrote:

Am Freitag, 14. März 2008 17:46 schrieben Sie:

...

I think that removing aliases completely is not a good idea. How about generating much lower aliases for decimals (lets say until 1000),

I don't think, this is a good idea. Like nobody will need an alias for 8247, nobody will need an alias for 824. The main point is that it is unnecessary to have a continuous range of numbers for which aliases exist. If you need aliases, you need them for "outstanding" values. Maybe you need aliases for all powers of 2 up to a certain number. Or aliases for all square numbers.

Therefore I think that if we want aliases then we should let the user and only the user generate them. This has also the interesting consequence that the type-level package doesn't need the Template Haskell language extension anymore. After all, using the template-haskell package doesn't imply that you have to have a TH-enabled compiler, as far as I know.

I don't agree. Not using aliases is a big pain, which means that every user wanting to use vectors with sizes biger than 10 (i.e. all) will have to generate their own alias set. It would be really annoying having to generate the aliases every time the library is used. Let's agree on a minimum alias set likely to be used by most of the users, small enough to get a reasonable object code size and compile time (we can even prevent haddock from parsing the alias module and just write a comment indicating what aliases are and which ones are generated if that helps). Generating type redefinitions up to decimal 500 shouldn't be such a big overhead (at least compared to the quntity of aliases generated right now).

...

droping the other bases,

That's a good idea.

...

and exporting a function to extended the alias range at will?

I'd rather propose something like this:

$(numAliasDecls [2 ^ n | n <- 0..16])

So that numAliasDecls has a type like [Int] -> [Decl].

That doesn't include bases, which might be important for the end user (for example Oleg wrote his type-evel numerical library in base 2 because it was aimed at system development). I'd rather propose a modification of Data.TypeLevel.Num.Aliases.genAliases which probably should be aware of the aliases already generated in the library so that they are not duplicated.