Re: Polymorphic Recursion / Rank-2 Confusion
Dominic Steinitz wrote:
> My motivation in using this type was to see if, for example, I could
> restrict addition of a vector to another vector to vectors of the same
> length. This would be helpful in the crypto library where I end up having to
> either define new length Words all the time or using lists and losing the
> capability of ensuring I am manipulating lists of the same length.
Perhaps you might find the following
http://pobox.com/~oleg/ftp/Haskell/number-parameterized-types.html
relevant to your task. The page demonstrates bitvectors of a
statically-checked width. An attempt to AND or OR two bitvectors
of different widths results in a type error. The width can be
specified in _decimal_ rather than in binary, which makes types
smaller and far easier to read. Type error messages also become more
comprehensible. To implement just the width-checking, we need only
Haskell 98.
Incidentally, the approach can be easily extended to arbitrary bases,
e.g., base64. Therefore, we can define numerals over a field Z^{*}_p
whose modulus p is statically known and statically checked. It would
be a type error to add or multiply two numerals with different
moduli. With base64-bigits, we need only 86 bigits for a 512-bit
modulus. Eighty-six terms make a type expression a bit long, but still
manageable; whereas binary types such as Zero and One would make
the approach unfeasible.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
On maandag, sep 22, 2003, at 00:07 Europe/Amsterdam, Brandon Michael Moore wrote: Can anyone tell me what's wrong with the following derivation? Without going through your derivation completely, the problem is almost certainly polymorphic recursion. Vector is a nested datatype---its definition calls itself with different type arguments---and so, although collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a] the recursive call to collect in, for example, the second clause, has a different type, namely: collect :: (v -> [a]) -> ((w,w) -> [a]) -> Vector v w -> [a] However, in the absence of an explicit type signature, Haskell will assume that the types of the top-level and recursive occurrences of collect are equal, which they are not, so you'll get a type error. Indeed, the error messages Dominic posted: > ERROR "Test1.hs":23 - Type error in function binding > *** Term : coal_ > *** Type : (a -> b) -> (c -> [d]) -> Vector_ a e -> b > *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> b > *** Because: unification would give infinite type > > Test1.hs:25: > Occurs check: cannot construct the infinite type: t = (t, t1) > Expected type: (t, t1) > Inferred type: t > In the first argument of `coalw', namely `w1' > In the first argument of `(++)', namely `(coalw w1)' corroborate this argument. Or, are you asking instead why it is that type inference does not work for polymorphic-recursive functions? Regards, Frank ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
On Sun, 21 Sep 2003, Dominic Steinitz wrote: > > Brandon, > > I get the error below without the type signature. My confusion was thinking > I needed rank-2 types. In fact I only need polymorphic recursion. Ross > Paterson's suggestion fixes the problem. I stole Even and Odd from Chris > Okasaki's paper on square matrices. They relate to fast exponentation > algorithm. There's something to be said for Zeror and One; as you say they > give the structure in binary. I would guess you knew you needed a forall, but missed the implicit one out front. I'm glad you got this working. I'm surprised this didn't typecheck though. I usually put signatures on top level functions, so I suppose my intuition is more tuned to types that can be checked rather than types that can be inferred. Can anyone tell me what's wrong with the following derivation? join :: (a -> [c]) -> (b -> [c]) -> ((a,b) -> [c]) join f g (x,y) = f x ++ g y collect_ colv colw (Zero v) = colv v collect_ colv colw (Odd v) = collect_ colv (join colw colw) v collect_ colv colv (Even v) = collect_ (join colv colw) (join colw colw) v for the first equation, name the type of collect_ collect_ :: t name the arguments and unify collect_ with the argument types colv :: a colw :: b (Zero v) :: Vector v w t = a -> b -> Vector v w -> d The type of v follows from the data type definition v :: v The body is an application (colv v), so we get a = c -> d, c = v so far we have collect :: (v -> d) -> b -> Vector v w -> d which uses up all the constraints. In the next equation v has type v :: Vector v (w,w) b = (e -> [f]) (from the type of join) for the recursive call to collect, we get constraints like d[(w,w)/w] = d (e->[f])[(w,w)/w] = ((e,e) -> [f]) We can deduce that w is not in the free variables of d or f, and that e = w. Now we have the type collect :: (v -> d) -> (w -> [f]) -> Vector v w -> d In the last equation the use of join lets us deduce that d = [f], giving a final type collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a]. What did I do wrong here? Probably the constraints between unification varaibles. Is there a problem with that sort of reasoning? I think I'm probably expecting some sort of implicit quantification that I haven't really specified. > My motivation in using this type was to see if, for example, I could > restrict addition of a vector to another vector to vectors of the same > length. This would be helpful in the crypto library where I end up having to > either define new length Words all the time or using lists and losing the > capability of ensuring I am manipulating lists of the same length. I've vaugely heard about something called Cryptol that Galois connections wrote, that compiles to Haskell. I don't know about the licensing status though. Brandon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
Ross, Thanks very much. I was going to use coal :: Vector a -> [a] coal = coal_ (\() -> []) (\x -> [x]) but I prefer your definitions. Dominic. - Original Message - From: "Ross Paterson" <[EMAIL PROTECTED]> To: "Dominic Steinitz" <[EMAIL PROTECTED]> Cc: <[EMAIL PROTECTED]> Sent: Saturday, September 20, 2003 5:19 PM Subject: Re: Polymorphic Recursion / Rank-2 Confusion > On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote: > > Can anyone tell me why the following doesn't work (and what I have to do to > > fix it)? I thought by specifying the type of coalw as rank-2 would allow it > > to be used both at a and (a,b). > > Change the signature to > > coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a] > > Then you can define > > type Vector = Vector_ () > > coal :: Vector a -> [a] > coal = coal_ (const []) (:[]) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
Brandon, I get the error below without the type signature. My confusion was thinking I needed rank-2 types. In fact I only need polymorphic recursion. Ross Paterson's suggestion fixes the problem. I stole Even and Odd from Chris Okasaki's paper on square matrices. They relate to fast exponentation algorithm. There's something to be said for Zeror and One; as you say they give the structure in binary. My motivation in using this type was to see if, for example, I could restrict addition of a vector to another vector to vectors of the same length. This would be helpful in the crypto library where I end up having to either define new length Words all the time or using lists and losing the capability of ensuring I am manipulating lists of the same length. Dominic. hugs Type checking ERROR "Test1.hs":23 - Type error in function binding *** Term : coal_ *** Type : (a -> b) -> (c -> [d]) -> Vector_ a e -> b *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> b *** Because: unification would give infinite type ghci Test1.hs:25: Occurs check: cannot construct the infinite type: t = (t, t1) Expected type: (t, t1) Inferred type: t In the first argument of `coalw', namely `w1' In the first argument of `(++)', namely `(coalw w1)' Failed, modules loaded: none. - Original Message - From: "Brandon Michael Moore" <[EMAIL PROTECTED]> To: "Dominic Steinitz" <[EMAIL PROTECTED]> Cc: <[EMAIL PROTECTED]> Sent: Saturday, September 20, 2003 11:19 PM Subject: Re: Polymorphic Recursion / Rank-2 Confusion > Sorry about the empty message. Send /= Cancel > > > Can anyone tell me why the following doesn't work (and what I have to do to > > fix it)? I thought by specifying the type of coalw as rank-2 would allow it > > to be used both at a and (a,b). > > Frank explained why the type you gave wouldn't work. I would like to add > that your function would type check without the type signature. This > suggests something here is actively confusing. Do you have any idea what > caused this problem? > > I hope to help teach Haskell to first year students, so I'm trying to > figure out what parts of the language are hard to get, and how to usefull > explain things. Anything in pure H98 that trips up an experienced > programmer is worth some attention. > > Completely unrelated, I think Zero and One would be better names than Even > and Odd because then the string of constructors writes the size of the > vector in binary, LSB first. I can't see any mnenomic value to Even and > Odd. How do you interpret Even and Odd? > > Thanks > > Brandon > ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
Sorry about the empty message. Send /= Cancel > Can anyone tell me why the following doesn't work (and what I have to do to > fix it)? I thought by specifying the type of coalw as rank-2 would allow it > to be used both at a and (a,b). Frank explained why the type you gave wouldn't work. I would like to add that your function would type check without the type signature. This suggests something here is actively confusing. Do you have any idea what caused this problem? I hope to help teach Haskell to first year students, so I'm trying to figure out what parts of the language are hard to get, and how to usefull explain things. Anything in pure H98 that trips up an experienced programmer is worth some attention. Completely unrelated, I think Zero and One would be better names than Even and Odd because then the string of constructors writes the size of the vector in binary, LSB first. I can't see any mnenomic value to Even and Odd. How do you interpret Even and Odd? Thanks Brandon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
On Sat, 20 Sep 2003, Ross Paterson wrote: > On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote: > > Can anyone tell me why the following doesn't work (and what I have to do to > > fix it)? I thought by specifying the type of coalw as rank-2 would allow it > > to be used both at a and (a,b). > > Change the signature to > > coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a] > > Then you can define > > type Vector = Vector_ () > > coal :: Vector a -> [a] > coal = coal_ (const []) (:[]) > ___ > Haskell mailing list > [EMAIL PROTECTED] > http://www.haskell.org/mailman/listinfo/haskell > > ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
On Sat, Sep 20, 2003 at 12:01:32PM +0100, Dominic Steinitz wrote: > Can anyone tell me why the following doesn't work (and what I have to do to > fix it)? I thought by specifying the type of coalw as rank-2 would allow it > to be used both at a and (a,b). Change the signature to coal_ :: (v -> [a]) -> (w -> [a]) -> Vector_ v w -> [a] Then you can define type Vector = Vector_ () coal :: Vector a -> [a] coal = coal_ (const []) (:[]) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Polymorphic Recursion / Rank-2 Confusion
On zaterdag, sep 20, 2003, at 13:01 Europe/Amsterdam, Dominic Steinitz wrote: Can anyone tell me why the following doesn't work (and what I have to do to fix it)? I thought by specifying the type of coalw as rank-2 would allow it to be used both at a and (a,b). This will never work. A function expecting a value of type forall c d. c -> [d] needs to be passed a function which can turn an arbitrary value of an arbitrary type into a list of values of every other, arbitrary type; the only such (total) function I can think of is const []. The type checker is complaining because the value you pass it is a function which only accepts tuple inputs; it has to work for _all_ inputs of any type. If you explain what you're trying to do here, maybe someone can suggest a solution. Regards, Frank ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Polymorphic Recursion / Rank-2 Confusion
Can anyone tell me why the following doesn't work (and what I have to do to
fix it)? I thought by specifying the type of coalw as rank-2 would allow it
to be used both at a and (a,b).
Dominic.
Reading file "Test.hs":tten
Type checking
ERROR "Test.hs":18 - Inferred type is not general enough
*** Expression: \(w1,w2) -> coalw w1 ++ coalw w2
*** Expected type : a -> [b]
*** Inferred type : (a,b) -> [c]
data Vector_ v w =
Zero v
| Even (Vector_ v (w,w))
| Odd (Vector_ (v,w) (w,w))
deriving Show
vzero = Zero ()
vone = Odd (Zero ((),'a'))
vtwo = Even (Odd (Zero ((),('a','b'
vthree = Odd (Odd (Zero (((),'a'),('b','c'
vfour = Even (Even (Odd (Zero ((),(('a','b'),('c','d'))
coal_ :: (forall a b. a -> [b]) ->
(forall c d. c -> [d]) ->
Vector_ v w -> [w]
coal_ coalv coalw (Zero v) =
coalv v
coal_ coalv coalw (Even v) =
coal_ coalv
(\(w1,w2) -> (coalw w1) ++ (coalw w2))
v
coal_ coalv coalw (Odd v) =
coal_ (\(v,w) -> (coalv v) ++ (coalw w))
(\(w1,w2) -> (coalw w1) ++ (coalw w2))
v
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
