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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
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 |
Free forum by Nabble | Edit this page |