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
Moving on to the implementation of fixed-sized vectors themselves ...

I have been trying to implement them as a GADT but I have run into
quite few problems. As a result, I'm considering to implement them
using the more-traditional phantom type-parameter approach. Anyhow,
I'd like to share those problems with the list, just in case someone
comes with a solution.

Here are some examples of what I was able to define without problems
(although, for some cases, I was forced to "break" the safety layer of
the GADT by using the toInt reflection function).

Save this email as FSVec.lhs to test them.

> {-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, KindSignatures #-}
> module Data.Param.FSVec where
>
> import Data.TypeLevel.Num

The Fixed Sized Vector data type. I know Wolfgang would prefer
something more closely named to LiSt to, but let's avoid getting into
that discussion now.

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

> infixr :>

Some successful examples

> headV :: Pos s => FSVec s a -> a
> headV (x :> xs) = x

> lastV :: Pos s => FSVec s a -> a
> lastV = lastV'
>   -- trusted function without the Pos constraint, otherwise the compiler would complain about
>   -- the Succ constraint of :> not being met.
>   where lastV' :: FSVec s a -> a
>         lastV' (x :> NullV) = x
>         lastV' (x :> xs)    = lastV' xs

> atV :: (Pos s, Nat n, n :<: s) => FSVec s a -> n -> a
> atV v n = atV' v (toInt n)
>   -- Reflecting the index breaks checking that the recursive call
>   -- verifies the atV constraints, however I couldn't find another way.
>   -- atV' is to be trusted regarding the recursive call
>   where atV' :: FSVec s a -> Int -> a
>         atV' (x :> xs) n
>          | n == 0       = x
>          | otherwise    = atV' xs (n-1)
> -- this defition is nicer but doesn't typecheck
> -- atV (x :> xs) n
> -- | toInt  n == 0 = x
> -- | otherwise = atV xs (predRef n)

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)

Tail function, which is also incorrect.

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

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.

Another alternative would be forcing the user to provide the size
explicitly (which is ugly as well)

vector' :: Nat s => s -> [a] -> FSVec s a

The Succ constraint in the definition of :> doesn't allow me to do
such a thing. The following implementation does not typecheck:

vector' :: Nat s => s -> [a] -> FSVec s a
vector' s l
 | toInt s == length l = vector' l
 | otherwise           = error "dynamic/static size mismatch"
   where vector'' :: [a] -> FSVec s a
              vector'' []        = NullV
              vector'' (x : xs)  = x :> vector' xs

The problem is that I don't know a way in which to "bypass" the Succ
constraint of :> .

Using a traditional phantom type-parameter to express the size is the
only solution I can think of (which would also solve the problems of
init and tail).  However, that would mean losing the ability of
pattern matching with (:>).

Any comments/suggestions would be very much appreciated.

Cheers,

Fons


[1] http://ofb.net/~frederik/vectro/draft-r2.pdf
_______________________________________________
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
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
_______________________________________________
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 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
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 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
Reply | Threaded
Open this post in threaded view
|

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

Dan Licata
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
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
Hi Wolfgang,


On Feb 10, 2008 5:43 PM, Wolfgang Jeltsch <[hidden email]> wrote:

I added some line annotations to the code below so that errors can be
more easily understood

> > (<+>) :: Add s1 s2 s3 => FSVec s1 a -> FSVec s2 a -> FSVec s3 a -- line 78
> > NullV  <+> ys  = ys -- line 79
> > (x:>xs) <+> ys = x :> (xs <+> ys) -- line 80
>
> 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.

I'm not sure if that is the only problem.

I already mentioned I'm a noob with GADTs so I might be wrong but it
seems that emulating dependent types with multiparameter type classes
or type synonym families (more on this below) and GADT pattern
matching does not work nicely.  In the case of <+>, three errors are
generated:

1)
    Couldn't match expected type `s3' against inferred type `s2'
      `s3' is a rigid type variable bound by
           the type signature for `<+>' at Data/Param/FSVec.hs:78:19
      `s2' is a rigid type variable bound by
           the type signature for `<+>' at Data/Param/FSVec.hs:78:16
      Expected type: FSVec s3 a
      Inferred type: FSVec s2 a

2)
    Could not deduce (Data.TypeLevel.Num.Sets.PosI s3,
                      Data.TypeLevel.Num.Ops.NClassify s3 yc,
                      Data.TypeLevel.Num.Ops.DivMod10 yh yl s3)
      from the context (Succ s11 s1)

3)
    Could not deduce (Data.TypeLevel.Num.Ops.Add' s11 s2 s,
                      Data.TypeLevel.Num.Ops.Add' s2 s11 s)
      from the context (Succ s11 s1)
      arising from a use of `<+>'


So defining the lema you mentioned (succ (x + y) = succ x + y)
wouldn't solve the whole problem. Actually (2) wouldn't happen if the
context of the function was taken into account (i.e.  "from the
context (Succ s11 s1)" should be "from the context (Succ s11 s1, Add
s1 s2 s3)". Can someone explain why GHC does not behave like that?


I don't know if type synonym families would help for <+> but certainly
they don't for tailV:


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


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.

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


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

* Positive part:
  - Operations on types can really be expressed as functions on types
which is more natural than using MTPC-constraints. Infox operands are
particularly expressive. For example:

-- Add type family
type family (:+:) x y :: *

 - According to
http://www.haskell.org/pipermail/haskell/2007-September/019759.html
They fit in a nicer way with the Haskell standard.

* Negative part:

  - They don't allow defining relational type operations, which is
_really_ important to dramatically reduce the number of necessary
instances.
 i.e Pred cannot be defined out of Succ, this declaration is ilegal

type family Pred x :: *
type instance Pred (Succ x) =  x

whereas it is perfecty possible using MTPCs

class (Pos x, Nat y) => Pred x y | x -> y, y -> x
instance Succ x y => Pred y x


 - 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

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 !

----
Conclusion
----

So, it seems that with or without type synonym families GADTs don't
work so nicely to emulate dependent types (or at least
numer-parameterized data structures), so I'll move on to traditional
phantom types unless someone provides a solution.

I'd like to be proven wrong (we'll lose pattern matching without GADTs
which is a pity) but I cannot come up with a better solution.

On the other hand, using phantom type parameters allows to encapsulate
whichever vector representation we want "under the hood".

And that's actually the approach followed by Fredrik Eaton's Vectro
library: http://ofb.net/~frederik/vectro/

So unless someone provides a solution for the GADT problem, I think
the best option would be simply adapting Vectro to work with the
type-level library.



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

Well, if that's all it can be done (and that's what it seems from your
answers), satisfied or not, there's no better option.


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

Best Regards,

A really frustrated Fons

PS:

Implemnetaion of Succ using a type synonym family.

-- | Successor type-level relation
type family Succ x :: *

type instance Succ D0 = D1
type instance Succ D1 = D2
type instance Succ D2 = D3
type instance Succ D3 = D4
type instance Succ D4 = D5
type instance Succ D5 = D6
type instance Succ D6 = D7
type instance Succ D7 = D8
type instance Succ D9 = (D1 :* D0)
type instance Succ (x :* D0) = x :* D1
type instance Succ (x :* D1) = x :* D2
type instance Succ (x :* D2) = x :* D3
type instance Succ (x :* D3) = x :* D4
type instance Succ (x :* D4) = x :* D5
type instance Succ (x :* D5) = x :* D6
type instance Succ (x :* D6) = x :* D7
type instance Succ (x :* D7) = x :* D8
type instance Succ (x :* D8) = x :* D9
type instance Succ (x :* D9) = (Succ x) :* D0

-- | value-level reflection function for the succesor type-level relation
--   (named succRef to avoid a clash with 'Prelude.succ')
succRef :: Nat x => x -> Succ x
succRef = undefined
_______________________________________________
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 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
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 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

> […]
_______________________________________________
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?)

Isaac Dupree
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
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
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
Reply | Threaded
Open this post in threaded view
|

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

Richard A. O'Keefe
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
Reply | Threaded
Open this post in threaded view
|

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

Dan Weston
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.

_______________________________________________
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
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
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
I asked Oleg regarding the use of GADTs to emulate dependent types. My
conclusion is that I should forget about them. Here is the full
answer:


---------- Forwarded message ----------
From:  <[hidden email]>
Date: Feb 12, 2008 8:49 AM
Subject: Re: GADTs to emulate dependent types?
To: [hidden email]



Hello!

> The main question is whether it is feasible to use GADTs to define
> fixed-sized vectors or not. The motivation behind it is to avoid
> needing to code your own trusted core and use the compiler typechecker
> for that purpose instead.

That is a false proposition. In Haskell, any code that uses GADT
*MUST* use a run-time test (run-time pattern match). Otherwise, the
code is unsound and provides no guarantees. The particular value of a
GADT data type is a witness of a proposition expressed in the type of
GADT (e.g., type equality). Since it is possible in Haskell to fake
this witness (just write undefined), if you don't check the witness at
run-time, that is, test that the witness is a real value rather than
undefined, you don't get any guarantees. That is why the irrefutable
pattern-match does not work with GADT. Incidentally, the first
implementation of GADT in GHC did permit irrefutable pattern-match,
which did let one write unsound code (that is, code that gave
segmentation fault):
       http://okmij.org/ftp/Haskell/GADT-problem.hs

The issue is not present in Coq, for example, whose core calculus is
sound and you cannot fake the evidence.

Thus, the unsoundness of Haskell (the presence of undefined) mandates
the run-time test for any code that uses GADT. So, GADTs are
fundamentally less efficient than the typeclasses; the latter can
provide assurances that can be checked at compile-time only, with no
run-time artifacts.

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

That is an old problem, and a difficult problem. In Singapore I was
talking to Zhaohui Luo (you can look him up on Google), who said that
the problem of asserting two types being equal (that is,
Succ D0 being equal to D1) is a very tough one. Conor McBride have
written a paper on observational equality -- but this is not
Haskell. So, I don't think this approach works.

       Cheers,
       Oleg
_______________________________________________
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 14, 2008 10:40 AM, Wolfgang Jeltsch <[hidden email]> 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?)
_______________________________________________
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
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
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
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
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
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
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
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.html#th-quasiquotation
[2] http://www.haskell.org/pipermail/template-haskell/2008-February/000655.html

On Wed, Feb 20, 2008 at 2:26 AM, Wolfgang Jeltsch
<[hidden email]> 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
>  [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?)

Wolfgang Jeltsch-2
Am Mittwoch, 20. Februar 2008 09:20 schrieben Sie:

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

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.  
Being a list of fixed size is not so important for vectors, in fact, it’s
completely unnecessary.  Real numbers are vectors, functions from real
numbers to real numbers are vectors, matrixes are vectors—you just have to
provide them with proper addition and scalar multiplication.  The data type
you defined is a fixed size list.

> […]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12345