# Implementing fixed-sized vectors (using datatype algebra?)

85 messages
12345
Open this post in threaded view
|

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

Open this post in threaded view
|

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

 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 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com Am Samstag, 9. Februar 2008 23:46 schrieben Sie: > 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. 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com Am Samstag, 9. Februar 2008 23:33 schrieben Sie: > 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. 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 In reply to this post by Wolfgang Jeltsch-2 > > 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. The type vector :: [a] -> FSVec s a doesn't make sense here: because s is universally quantified at the outside, this says "for all lengths s, given a list, I can produce a vector of length s". And indeed, in the second version, it looks like you're using the continuation to curry an existential: vector :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w is the same as vector :: [a] -> ((exists s . Nat s and FSVec s a) -> w) -> w So why not just do vector :: [a] -> (exists s . Nat s and FSVec s a) I.e. data UnknownLengthVec a where   U :: Nat s => FsVec s a -> UnknownLengthVec a vector :: [a] -> UnknownLengthVec a I haven't tried, but I'd be surprised if you couldn't write this function by recuring on the list. Of course, this type does not relate the size of the vector to the output of the length function on lists; it just says you get a vector some size.  But maybe that's good enough for many uses? -Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

Open this post in threaded view
|

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

 In reply to this post by Dan Licata Hi Dan, On Feb 10, 2008 6:08 PM, Dan Licata <[hidden email]> 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_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

Open this post in threaded view
|

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

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com 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! _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 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. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

Open this post in threaded view
|

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

 Am Donnerstag, 14. Februar 2008 03:23 schrieben Sie: > To directly answer Wolfgang's question: "parameterized" is the more > common. It is "more correct" only insofar as it is the more common. So we should “parameterized” for the package name. Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

Open this post in threaded view
|

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

Open this post in threaded view
|

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

 Am Dienstag, 19. Februar 2008 21:44 schrieben Sie: > * Support of type-level Booleans (Wolfgang?) 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. Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe Boolean.hs (3K) Download Attachment
Open this post in threaded view
|

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

 2008/2/19 Wolfgang Jeltsch <[hidden email]>: > 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

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

 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|