On 25.06.10 20:09, Jason Dagit wrote:
you got everything right here. So, as you said, there is a mismatch
between representation in Haskell (list of code points) and
representation in the operating system (list of bytes), so we need to
know the encoding. Encoding is supplied
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type levels, then you should look
into dependently typed languages.
Out of curiosity, what the hell does dependently typed mean anyway?
On 26 June 2010 08:07, Andrew Coppin andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
How about:
The result type of a function may depend on the argument value
(rather than just the argument type)
The quoted bit rather than the parens bit
It means that not only can values have types, types can have values.
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Due to the curry-howard isomorphism, dependent types open the gateway
for lots of type-level theorem proving.
On 26 June 2010
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin andrewcop...@btinternet.com
wrote:
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type levels, then you should look into
dependently typed languages.
Out of
On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
andrewcop...@btinternet.com wrote:
wren ng thornton wrote:
And, as Jason said, if you're just interested in having the same
programming style at both term and type
I whipped up a little Emacs script to align the import lines in the
current buffer. I am using it in my projects and have experienced no
problems. It's good at keeping within 80 columns.
http://gist.github.com/453933
I've pasted it as a gist on Github so that anyone can edit it, gists
also
That's really nice. Very interesting. Thank you.
On Fri, Jun 25, 2010 at 9:55 PM, Edward Kmett ekm...@gmail.com wrote:
I've obtained permission to repost Gershom's slides on how to deserialize
GADTs by typechecking them yourself, which are actually a literate haskell
source file, that he was
Liam O'Connor wrote:
It means that not only can values have types, types can have values.
Uh, don't types have values *now*?
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Oh, right. So you mean that as well as being able to say Foo
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Andrew Coppin wrote:
Liam O'Connor wrote:
It means that not only can values have types, types can have values.
Uh, don't types have values *now*?
An example of the uses of a dependent type would be to encode the
length of a list in it's type.
Jason Dagit wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
andrewcop...@btinternet.com mailto:andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
The types can depend on values. For example, have you ever notice we
have
Tony Morris wrote:
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Ah yes, it was definitely Epigram I looked at. The intro to this looked
promising, but by about 3 pages in, I had absolutely no clue what on
Earth the text is talking about...
___
On Sat, Jun 26, 2010 at 3:49 AM, wren ng thornton w...@freegeek.org wrote:
Jason Dagit wrote:
On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety
black.m...@gmail.comwrote:
I've noticed over the - okay, over the months - that some folks enjoy the
puzzle-like qualities of programming in the
Hello Gábor,
Saturday, June 26, 2010, 4:29:28 PM, you wrote:
It's interesting how C++ is imperative at the term level and
functional at the type level
or logic? it supports indeterminate choice
--
Best regards,
Bulatmailto:bulat.zigans...@gmail.com
On Sat, Jun 26, 2010 at 09:29:29AM +0300, Roman Beslik wrote:
Incorrect encoding of filepaths is common in e.g. Cyrillic Linux
(because of multiple possible encodings --- CP1251, KOI8-R, UTF-8)
and is solved by fiddling with the current locale and media mount
options. No need to change a
Hello Felipe,
Saturday, June 26, 2010, 4:44:20 PM, you wrote:
Even if we said we don't care, we at least should change
FilePath to be [Word8], and not [String]. Currently filepaths
are silently truncated if any codepoint is beyond 255.
and there is no OS except Unix ;)
--
Best regards,
On Sat, Jun 26, 2010 at 04:48:39PM +0400, Bulat Ziganshin wrote:
Saturday, June 26, 2010, 4:44:20 PM, Felipe Lessa wrote:
Even if we said we don't care, we at least should change
FilePath to be [Word8], and not [String]. Currently filepaths
are silently truncated if any codepoint is beyond
I prefer Agda to Epigram, but different strokes for different folks.
In agda, you could define a list indexed by its size like this:
data Vec : (A : Set) → ℕ → Set where
[] : Vec A 0
_∷_ : ∀ {n : ℕ} → A → Vec A n → Vec A (1 + n)
So, we have a Vec data type, and on the type level it is a
We most certainly do have type-level functions. See type families.
Cheers.
~Liam
On 26 June 2010 17:33, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:27 AM, Jason Dagit da...@codersbase.com wrote:
On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin
Hello Felipe,
Saturday, June 26, 2010, 4:54:16 PM, you wrote:
Even if we said we don't care, we at least should change
FilePath to be [Word8], and not [String]. Currently filepaths
other OSs worked fine, should I use this API (i.e. type FilePath
= String) to its fullest extent, my
On Sat, Jun 26, 2010 at 05:01:06PM +0400, Bulat Ziganshin wrote:
Even if we said we don't care, we at least should change
FilePath to be [Word8], and not [String]. Currently filepaths
other OSs worked fine, should I use this API (i.e. type FilePath
= String) to its fullest extent, my
On Sat, 26 Jun 2010 10:14:50 -0300
Felipe Lessa felipe.le...@gmail.com wrote:
On Sat, Jun 26, 2010 at 05:01:06PM +0400, Bulat Ziganshin wrote:
but what you propose cannot be used in Windows at all! while current
FilePath still works on Unix, with manual filenames en/decoding
Now we got
Hi all,
At the moment, I'm learning haskell and I would like to use the things
I'm learning under web.
I would like to mount a local web server, but I would like to test some
things in my VPS in 11 with CentOs 5, but this, in a near future.
For the moment, my doubt is, wich is the haskell
On Sat, Jun 26, 2010 at 05:34:49PM +0400, Alexey Khudyakov wrote:
It should solve most of problems I believe. But such change will break
a lot of programs maybe most of them. How could one introduce such a
change? One variant is to create new hierarchy and gradually deprecate
old.
Also same
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Uh, don't types have values *now*?
To the extent that's true now, they're baked in; you can't do anything
to/with them.
Oh, right. So you mean that as well as being able to say Foo Bar, you can
say Foo 7,
On Sat, Jun 26, 2010 at 3:27 AM, Jason Dagit da...@codersbase.com wrote:
The types can depend on values. For example, have you ever notice we have
families of functions in Haskell like zip, zip3, zip4, ..., and liftM,
liftM2, ...?
Each of them has a type that fits into a pattern, mainly the
On Jun 26, 2010, at 4:33 AM, Andrew Coppin wrote:
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
common knowledge.
A first order logic quantifies over values, and a second order logic
quantifies
Attached is a program with a space leak that I do not understand. I have
coded a simple 'map' function, once using unsafePerformIO and once
without. UnsafePerformIO has a space leak in some circumstances. In the
main program I demonstrate cases with and without space leak. Without
space leak the
John Lato wrote:
How would you implement bfnum? (If you've already read the paper,
what was your first answer?)
My first idea was something similar to what is described in appendix A.
However, after reading the paper, I wrote the following code:
data Tree a = E | T a (Tree a) (Tree a)
Alexander Solla wrote:
On Jun 26, 2010, at 4:33 AM, Andrew Coppin wrote:
It's a bit like trying to learn Prolog from somebody who thinks that
the difference between first-order and second-order logic is somehow
common knowledge.
A first order logic quantifies over values, and a second
Brandon S Allbery KF8NH wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Oh, right. So you mean that as well as being able to say Foo Bar, you can
say Foo 7, where 7 is (of course) a value rather than a type. (?)
A bit more than that:
mauke from the Freenode IRC channel has contributed a vim version:
http://gist.github.com/454255
On 26 June 2010 12:25, Christopher Done chrisd...@googlemail.com wrote:
I whipped up a little Emacs script to align the import lines in the
current buffer. I am using it in my projects and have
On Sat, Jun 26, 2010 at 11:23 AM, Andrew Coppin andrewcop...@btinternet.com
wrote:
Brandon S Allbery KF8NH wrote:
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 07:28 , Andrew Coppin wrote:
Oh, right. So you mean that as well as being able to say Foo Bar, you
can
say Foo 7,
On Jun 26, 2010, at 11:21 AM, Andrew Coppin wrote:
A first order logic quantifies over values, and a second order
logic quantifies over values and sets of values (i.e., types,
predicates, etc). The latter lets you express things like For
every property P, P x. Notice that this
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 14:58 , Jason Dagit wrote:
On Sat, Jun 26, 2010 at 11:23 AM, Andrew Coppin andrewcop...@btinternet.com
mailto:andrewcop...@btinternet.com wrote:
Brandon S Allbery KF8NH wrote:
A bit more than that: imagine now that you can
Andrew Coppin wrote:
Right, I see.
So is there a specific reason why Haskell isn't dependently typed then?
One problem with dependent types as I understand it is that type
inference is not guaranteed to terminate.
Erik
--
On Sat, Jun 26, 2010 at 6:55 PM, Erik de Castro Lopo
mle...@mega-nerd.com wrote:
One problem with dependent types as I understand it is that type
inference is not guaranteed to terminate.
Full type inference is undecidable in most interesting type systems
anyway. It's possible for the
On 26.06.10 16:34, Alexey Khudyakov wrote:
On Sat, 26 Jun 2010 10:14:50 -0300
Felipe Lessafelipe.le...@gmail.com wrote:
On Sat, Jun 26, 2010 at 05:01:06PM +0400, Bulat Ziganshin wrote:
but what you propose cannot be used in Windows at all! while current
FilePath still works on Unix, with
On 26.06.10 15:44, Felipe Lessa wrote:
On Sat, Jun 26, 2010 at 09:29:29AM +0300, Roman Beslik wrote:
Incorrect encoding of filepaths is common in e.g. Cyrillic Linux
(because of multiple possible encodings --- CP1251, KOI8-R, UTF-8)
and is solved by fiddling with the current locale and media
On Sun, Jun 27, 2010 at 02:55:33AM +0300, Roman Beslik wrote:
On 26.06.10 15:44, Felipe Lessa wrote:
However, suppose your program needs to create a file with a name
based on a database information. Your database is UTF-8. How do
you translate that UTF-8 data into a filepath? This is the
On Sun, Jun 27, 2010 at 02:52:54AM +0300, Roman Beslik wrote:
On 26.06.10 16:34, Alexey Khudyakov wrote:
On Sat, 26 Jun 2010 10:14:50 -0300
Felipe Lessafelipe.le...@gmail.com wrote:
On Sat, Jun 26, 2010 at 05:01:06PM +0400, Bulat Ziganshin wrote:
but what you propose cannot be used in
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 6/26/10 19:52 , Roman Beslik wrote:
I fail to see how it will brake programs. Current programs do not use
Unicode because it is implemented incorrectly.
Currently, FilePath is an alias for String. Changing FilePath to a real
type will break
On Sat, Jun 26, 2010 at 10:01:57PM -0300, Felipe Lessa wrote:
The types are:
getArgs :: IO [String]
writeFile :: FilePath - String - IO ()
On a similar note, getArgs probably suffers from the same
problem. Which should it be?
a) getArgs :: IO [String]
b) getArgs :: IO [Word8]
c)
Gregory Crosswhite wrote:
On 6/25/10 9:49 PM, wren ng thornton wrote:
[1] http://eclipse-clp.org/ is currently down, but can be accessed at
http://87.230.22.228/
[2] http://www.mercury.csse.unimelb.edu.au/
[3] http://www.lix.polytechnique.fr/~dale/lProlog/
[4]
Andrew Coppin wrote:
Stephen Tetley wrote:
On 26 June 2010 08:07, Andrew Coppin andrewcop...@btinternet.com wrote:
Out of curiosity, what the hell does dependently typed mean anyway?
How about:
The result type of a function may depend on the argument value
(rather than just the argument
Andrew Coppin wrote:
I think I looked at Coq (or was it Epigram?) and found it utterly
incomprehensible. Whoever wrote the document I was reading was obviously
very comfortable with advanced mathematical abstractions which I've
never even heard of.
One of the things I've found when dealing
46 matches
Mail list logo
