[Haskell] Fixed-length vectors in Haskell
David Menendez wrote:
] data Vec n a where
] Nil :: Vec Zero a
] Cons :: a -> Vec n a -> Vec (Succ n) a
] data Vec_0 a = Nil
] data Vec_s v a = Cons a (v a)
Ashley Yakeley wrote:
] vcons a v Zero = a
] vcons a v (Succ n) = v n
S.M.Kahrs wrote:
] data Cons b a = a :. b a
] data NIL a = NIL
There is a common pattern in all these approaches to fixed-length
vectors: using *data* constructors to encode particular properties of
the data structure. This approach goes back to Chris Okasaki (``From
fast exponentiation to square matrices: An adventure in types.''
ICFP'99), who showed constructing not only of fixed-size vectors but
also matrices that are guaranteed to be square. He also showed
(quoting Ross Paterson, 1998) how to construct an AVL tree so that the
AVL invariant is enforced by construction:
http://www.haskell.org/pipermail/haskell/2003-April/011693.html
This approach has the immense advantage that the invariant cannot be
broken at all. One just can't have a list with fewer Cons cells than
there are elements in the list. Chris Okasaki (in the above message)
has also pointed out a drawback: all these data constructors take
space to be present in memory, and take time to traverse. So, in all
the above representations, to take the 1023d element of a 1024-element
vector, we have to traverse 1023 Cons cells.
The alternative is to encode the invariant -- the vector size, in our
problem -- in *type* constructors, in phantom types. For example,
> newtype PVector n a = PVector (Array Int a)
The run-time representation of PVector n a is the same as Array Int a,
which is quite efficient. There are no traces of the `Nat' can be
found: we use the type-level invariant for type-checking only. So, we
get additional assurances without distorting data structures and
without any run-time penalty whatsoever.
The drawback and the advantage of phantom types is that they are not
``bound'', so to speak, to a term -- they are just ``attached.'' If
the user gets hold of the PVector constructor, the user can easily
compromise our invariants. So, we have to hide PVector in a module and
expose only functions that build the values of PVector one way or the
other. We also have to make sure that these functions are correct --
because they constitute the trusted kernel of our invariant. The
advantage of that approach is that we can implement very flexible
invariants. Come to think of it, this approach isn't that far from
LCF.
David Menendez wrote:
] We would like a function "vec :: a -> Vec n a", such that "vec x"
] returns a vector of length n with every element equal to x. The basic
] algorithm is simple:
]
] vec{0} x = Nil
] vec{n+1} x = Cons x (vec{n} x)
]
] The usual way to declare a function like this involves a type class,
] which lets us define functions with different behaviors for different
] types:
]
] class Nat n where vec :: a -> Vec n a
]
] instance Nat Zero where vec x = Nil
] instance Nat n => Nat (Succ n) where vec x = Cons x (vec x)
]
] This gives vec the type "Nat n => a -> Vec n a", which is good because
] it points out that the type argument to Vec must be a natural, formed
] from Zero or Succ applied to another natural.
]
] However, this solution is unsatisfactory, because it requires the Nat
] class to include every possible function which might depend on a
] type-level argument.
Actually it is not that difficult to create a Nat class with ``every
possible function'' as a member:
> class Nat' n e f where doit :: e a -> f n a
> newtype VecFN n a = VecFN (Vec n a)
> newtype ID a = ID a
> unVecFN (VecFN x) = x
> unID (ID x) = x
> instance Nat' Zero ID VecFN where doit (ID a) = VecFN Nil
> instance Nat' n ID VecFN => Nat' (Succ n) ID VecFN where
> doit (ID a) = VecFN (Cons a (unVecFN $ doit (ID a)))
> vec' :: Nat' n ID VecFN => a -> Vec n a
> vec' = unVecFN . doit . ID
*Vector_GADT> vec' 2 :: (Vec Three Int)
[2,2,2]
If we wish now to implement fromList function, we do
> newtype FromList' n a = FromList'
> { runFromList' :: Maybe (Vec n a) }
>
> fromList' :: Nat' n [] FromList' => [a] -> Maybe (Vec n a)
> fromList' = runFromList' . doit
>
> instance Nat' Zero [] FromList' where doit = \l -> FromList' $ Just Nil
> instance Nat' n [] FromList' => Nat' (Succ n) [] FromList' where
> doit = \l -> case l of
>x:xs -> FromList' (fmap (Cons x) (runFromList' $ doit xs))
>[] -> FromList' Nothing
*Vector_GADT> fromList' [1,2,3] :: (Maybe (Vec Three Int))
Just [1,2,3]
*Vector_GADT> fromList' [1,2] :: (Maybe (Vec Three Int))
Nothing
This tagging and untagging may be a bit annoying. OTH, FromList', ID,
etc. are all newtypes.
Ashley Yakeley wrote:
] > impossible :: Empty -> a
] > impossible _ = undefined
]
] It's unfortunate that we can't define impossible without using bottom. I
] dislike using bottom, and here we have a function that cannot return
] bottom unless it is passed bottom. Such fu
[Haskell] ANNOUNCE: Haskell Communities & Activities Report (8th ed., May 2005)
On behalf of the many, many contributors, I am pleased to announce that the Haskell Communities and Activities Report (8th edition, May 2005) http://www.haskell.org/communities/ is now available from the Haskell Communities home page in several formats: PDF, for screenreading as well as printing, HTML, for those of you who prefer not to deal with plugins or external viewers, and PostScript, for those of you who have nice quick printers that do not grok PDF. Many thanks go to all the people that contributed to this report, both directly, by sending in descriptions, and indirectly, by doing all the interesting things that are reported. I hope you will find it as interesting a read as we did. If you haven't encountered the Haskell Communities and Activities Reports before, you may like to know that the first of these reports was published in November 2001. Their goal is to improve the communication between the increasingly diverse groups, projects and individuals working on, with, or inspired by Haskell. The idea behind these reports is simple: Every six months, a call goes out to all of you enjoying Haskell to contribute brief summaries of your own area of work. Many of you respond (eagerly, unprompted, and well in time for the actual deadline ;) ) to the call. The editor collects all the contributions into a single report and feeds that back to the community. When we try for the next update, six months from now, you might want to report on your own work, project, research area or group as well. So, please put the following into your diaries now: End of October 2005: target deadline for contributions to the November 2005 edition of the HC&A Report Unfortunately, many Haskellers working on interesting projects are so busy with their work that they seem to have lost the time to follow the Haskell related mailing lists and newsgroups, and have trouble even finding time to report on their work. If you are a member, user or friend of a project so burdened, please find someone willing to make time to report and ask them to `register' with the editor for a simple e-mail reminder in the middle of October (you could point us to them as well, and we can then politely ask if they want to contribute, but it might work better if you do the initial asking). Of course, they will still have to find the ten to fifteen minutes to draw up their report, but maybe we can increase our coverage of all that is going on in the community. Feel free to circulate this announcement further in order to reach people who might otherwise not see it. Enjoy! Andres Loeh -- Haskell Communities and Activities Report (http://haskell.org/communities) ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] HGetChar socket reading
hey guys ! I´m pretty nu to haskell, and i got the following things to do: code a client in python that sends string ->done code a server in haskell that recieves string -> to do... i initialized the server, set up a socket on port 9900, so the socket is allready open... First i read the string with hGetLine: loop socket = do (handle, host, port) <- accept socket forkIO (client handle) loop socket client handle = do query <- hGetLine handle this worked pretty good. Now my Tutor said, I should code this whole thing with hGetChar instead of hGetLine... I ain´t got the clue of an clue how to manage this... I worked something out like: client handle = do query <- hGetChar handle if query = [] then return(0) else let list = list ++ query I don´t know where the string is stored in the handle, and how to read it out...I mean, I can´t use stuff like query handle <- hGetChar(firstfrom:query handle)... Please Help Me !!! ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
Tony Finch <[EMAIL PROTECTED]> writes:
>> But they don't differ in addressing. In BSD sockets the difference
>> between streams and packets lies in "socket type", while addresses
>> are split into "address families" which bijectively correspond to
>> "protocol families".
>
> I believe there are some obscure protocol families that have more than
> one address family, which is why the two concepts exist in the API.
Single Unix Specification v3 specifies only AF_* constants, used for
both.
Linux man socket says:
NOTE
The manifest constants used under BSD 4.* for protocol families are
PF_UNIX, PF_INET, etc., while AF_UNIX etc. are used for address fami-
lies. However, already the BSD man page promises: "The protocol family
generally is the same as the address family", and subsequent standards
use AF_* everywhere.
--
__("< Marcin Kowalczyk
\__/ [EMAIL PROTECTED]
^^ http://qrnik.knm.org.pl/~qrczak/
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
On Thu, 12 May 2005, Marcin 'Qrczak' Kowalczyk wrote: > > But they don't differ in addressing. In BSD sockets the difference > between streams and packets lies in "socket type", while addresses > are split into "address families" which bijectively correspond to > "protocol families". I believe there are some obscure protocol families that have more than one address family, which is why the two concepts exist in the API. However there's an enormous amount of code that muddles them up, but this doesn't matter for the Internet protocols. Tony. -- f.a.n.finch <[EMAIL PROTECTED]> http://dotat.at/ BISCAY: WEST 5 OR 6 BECOMING VARIABLE 3 OR 4. SHOWERS AT FIRST. MODERATE OR GOOD. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
Einar Karttunen wrote: But what URI should represent e.g. unix datagram sockets? Having an URI connection function would be nice, but having it as the primary alternative would not be very nice. Could URI schemes like those in the Java Generic Connection Framework (see: http://developers.sun.com/techtopics/mobility/midp/articles/genericframework/ ) help unify things? - Ravi Nanavati ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
Peter Simons <[EMAIL PROTECTED]> writes:
> >> [URIs might be the answer]
>
> > But what URI should represent e.g. unix datagram sockets?
>
> I don't think it's worth even trying to hide both stream-
> and packet-oriented services behind the same API. These are
> completely different things, treated them differently is
> fine, IMHO.
But they don't differ in addressing. In BSD sockets the difference
between streams and packets lies in "socket type", while addresses
are split into "address families" which bijectively correspond to
"protocol families".
--
__("< Marcin Kowalczyk
\__/ [EMAIL PROTECTED]
^^ http://qrnik.knm.org.pl/~qrczak/
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Existing Haskell IPv6 Code
Einar Karttunen writes: >> Well, I certainly _do_ need [a representation of network >> addresses in Haskell]. > You can certainly get it: > getHost mySocketAddress niNumerichost > getServ mySocketAddress niNumericserv Um, yes, but 'String' isn't a very good representation for manipulating network addresses, IMHO. >> [URIs might be the answer] > But what URI should represent e.g. unix datagram sockets? I don't think it's worth even trying to hide both stream- and packet-oriented services behind the same API. These are completely different things, treated them differently is fine, IMHO. Peter ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
Peter Simons <[EMAIL PROTECTED]> writes: > > Lifting [network address information] to Haskell level > > seems quite pointless, as it is usually just fed back to > > the C functions. > > Well, I certainly _do_ need it. You can certainly get it: getHost mySocketAddress niNumerichost getServ mySocketAddress niNumericserv > That's true. However, it doesn't work with anything _but_ > IPv4 and IPv6. I think it is unsatisfactory that you need a > different function to connect to a TCP target than to > connect to a Unix stream socket. Having a separate TCP connect function is just for niceness - of course one can use an aproach to go from URIs to sockets having a case statement for each scheme. But what URI should represent e.g. unix datagram sockets? Having an URI connection function would be nice, but having it as the primary alternative would not be very nice. - Einar Karttunen ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
At 14:05 12/05/05 +0200, Peter Simons wrote: The longer I think about this whole thing, the more I am convinced that using URIs is the answer. FWIW, the revised URI parsing code [2][3] in the latest libraries includes support for IPv6 literals, as specified by RFC 3986 [1]. #g -- [1] ftp://ftp.rfc-editor.org/in-notes/rfc3986.txt [2] http://www.haskell.org/ghc/docs/latest/html/libraries/network/Network.URI.html [3] http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/libraries/network/Network/URI.hs Graham Klyne For email: http://www.ninebynine.org/#Contact ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Doctoral Studentships in Computing Science
Doctoral Studentships in Computing Science Oxford University Computing Laboratory (CancerGrid) Microsoft Research Applications are invited for two doctoral studentships at the University of Oxford, starting in October 2005, in the areas of: * object models * web services The students will be working alongside other members of the Software Engineering Research Group (www.softeng.ox.ac.uk). A focus for the research activity will be the Medical Research Council (MRC)-funded CancerGrid project (www.cancergrid.org), an ideal environment for applying, investigating, and extending modern software engineering techniques. There will also be opportunities for collaboration with Microsoft Research, Cambridge, who are providing financial support, together with the e-Science Centres at the Universities of Oxford and Cambridge. The studentships will cover all university fees at the `home' rate, and provide a student stipend equivalent to a standard EPSRC award. Applicants will need to satisfy the selection criteria for doctoral students in computing science at Oxford web.comlab.ox.ac.uk/oucl/prospective/dphil/dphil-criteria.pdf The closing date for applications is 1st July 2005. For further information and details of how to apply, please contact Jim Davies ([EMAIL PROTECTED]) or Jeremy Gibbons ([EMAIL PROTECTED]). -- [EMAIL PROTECTED] Oxford University Computing Laboratory,TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Existing Haskell IPv6 Code
Einar Karttunen writes: > Lifting [network address information] to Haskell level > seems quite pointless, as it is usually just fed back to > the C functions. Well, I certainly _do_ need it. > The current way is to ignore adress families as much as > possible while still supporting multiple ones. E.g. the > following works with both IPv4 and IPv6 in network-alt: > > googleMainPage = do > h <- connectTCP "www.google.com" "http" That's true. However, it doesn't work with anything _but_ IPv4 and IPv6. I think it is unsatisfactory that you need a different function to connect to a TCP target than to connect to a Unix stream socket. The longer I think about this whole thing, the more I am convinced that using URIs is the answer. Peter ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Existing Haskell IPv6 Code
Peter Simons <[EMAIL PROTECTED]> writes: > Judging from a quick glance, the code seems to marshal the > POSIX API: > > type SockAddrLen = Int > data SockAddrT > type SockAddr = ForeignPtr SockAddrT > data SocketAddress = SA !SockAddr !SockAddrLen > > I'm not sure whether that's a useful representation. It > works, of course, but it appears that an address is > essentially opaque (unless you want to do more FFI things). > It doesn't really unify different types of network addresses > either. Note, for example, that you can't pass such an > address to the 'connectTCP' function. That is one of the few working representations. The user of the library is not aware how the socket addresses are represented internally, so it is not a problem. Lifting the information to Haskell level seems quite pointless, as it is usually just fed back to the C functions. Also IPv6 addresses sometimes need scopes - lifting this would make things even more messy. The current way is to ignore adress families as much as possible while still supporting multiple ones. E.g. the following works with both IPv4 and IPv6 in network-alt: googleMainPage = do h <- connectTCP "www.google.com" "http" hPutStr h "GET / HTTP/1.0\r\n\r\n" hFlush h hGetContents h >>= print hClose h - Einar Karttunen ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
