Re: [Haskell-cafe] Core packages and locale support
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 by the user via locale (https://secure.wikimedia.org/wikipedia/en/wiki/Locale), particularly LC_CTYPE variable. The problem with encodings is not new -- it was already solved e.g. for input/output. This is the part where I don't understand the problem well. I thought that with IO the program assumes the locale of the environment but that with filepaths you don't know what locale (more specifically which encoding) they were created with. So if you try to treat them as having the locale of the current environment you run the risk of misunderstanding their encoding. 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 program, or to tell character encoding to a program. It is not a programming language issue. -- Best regards, Roman Beslik. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 is from Lennart Augustsson's Cayenne - a language with dependent types The papers on Cayenne might be an interesting start point as the field was less mature at that time, so the early papers had more explaining to do. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 17:07, 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 curiosity, what the hell does dependently typed mean anyway? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 curiosity, what the hell does dependently typed mean anyway? 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 arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. That of course, is only the tip of the iceberg. Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work. Even the example I just gave can be emulated. See this paper: http://www.brics.dk/RS/01/10/ Also SHE: http://personal.cis.strath.ac.uk/~conor/pub/she/ Then there are languages like Coq and Agda that support dependent types directly. There you can return a type from a function instead of a value. Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 levels, then you should look into dependently typed languages. 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 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 arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. That of course, is only the tip of the iceberg. Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work. Even the example I just gave can be emulated. See this paper: http://www.brics.dk/RS/01/10/ Also SHE: http://personal.cis.strath.ac.uk/~conor/pub/she/ Then there are languages like Coq and Agda that support dependent types directly. There you can return a type from a function instead of a value. I just realized, I may not have made this point sufficiently clear. Much of the reason we need to do extra work in Haskell to emulate dependent types is because types are not first class in Haskell. We can't write terms that manipulate types (type level functions). Instead we use type classes as sets of types and newtypes/data in place of type level functions. But, in dependently typed languages types are first class. Along this line, HList would also serve as a good example of what you would/could do in a dependently type language by showing you how to emulate it in Haskell. Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Emacs script to align Haskell import list
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 provide a simple revision history and comment support. Please feel free to contribute some tweaks and fixes. I'll then see about merging this into haskell-mode in some fashion. It doesn't handle multiple line explicit imports as I have a personal rule that any explicit import list with more than a few symbols should be changed to an as X import, as an addition to tibbe's style guide.[1] I haven't decided on a recommended keybinding. I'm considering a context-dependent binding of C-c C-. that indents the import list when you are on an import line. [1]: http://github.com/tibbe/haskell-style-guide ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)
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 rendering to slides. Consequently, I've just pasted
the content below as a literate email.
-Edward Kmett
-
Deserializing strongly typed values
(four easy pieces about typechecking)
Gershom Bazerman
-
prior art:
Oleg (of course)
http://okmij.org/ftp/tagless-final/course/course.html
...but also
Stephanie Weirich
http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs
=
Ahem...
\begin{code}
{-# LANGUAGE DeriveDataTypeable,
ExistentialQuantification,
FlexibleContexts,
FlexibleInstances,
FunctionalDependencies,
GADTs,
RankNTypes,
ScopedTypeVariables
#-}
\end{code}
=
ahem.
\begin{code}
import Data.Typeable
import Data.Maybe
import Control.Monad.Error
import Control.Applicative
import qualified Data.Map as M
import Unsafe.Coerce
\end{code}
=
A simple ADT.
\begin{code}
data SimpleExpr = SOpBi String SimpleExpr SimpleExpr
| SOpUn String SimpleExpr
| SDbl Double
| SBool Bool deriving (Read, Show, Typeable)
\end{code}
Yawn.
=
An awesome GADT!
\begin{code}
data Expr a where
EDbl :: Double - Expr Double
EBool :: Bool - Expr Bool
EBoolOpBi :: BoolOpBi - Expr Bool - Expr Bool - Expr Bool
ENumOpBi :: NumOpBi - Expr Double - Expr Double - Expr Double
ENumOpUn :: NumOpUn - Expr Double - Expr Double
deriving Typeable
data NumOpBi = Add | Sub deriving (Eq, Show)
data NumOpUn = Log | Exp deriving (Eq, Show)
data BoolOpBi = And | Or deriving (Eq, Show)
\end{code}
The GADT is well typed. It cannot go wrong.
-
It also cannot derive show.
=
But we can write show...
\begin{code}
showIt :: Expr a - String
showIt (EDbl d) = show d
showIt (EBool b) = show b
showIt (EBoolOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpBi op x y) = ( ++ show op
++ ++ showIt x
++ ++ showIt y ++ )
showIt (ENumOpUn op x) = show op ++ ( ++ showIt x ++ )
\end{code}
=
And eval is *much nicer*.
It cannot go wrong -- no runtime typechecks.
\begin{code}
evalIt :: Expr a - a
evalIt (EDbl x) = x
evalIt (EBool x) = x
evalIt (EBoolOpBi op expr1 expr2)
| op == And = evalIt expr1 evalIt expr2
| op == Or = evalIt expr2 || evalIt expr2
evalIt (ENumOpBi op expr1 expr2)
| op == Add = evalIt expr1 + evalIt expr2
| op == Sub = evalIt expr1 - evalIt expr2
\end{code}
=
But how do we write read!?
read EBool False = Expr Bool
read EDbl 12 = Expr Double
The type being read depends on the content of the string.
Even worse, we want to read not from a string that looks obvious
to Haskell (i.e. a standard showlike instance) but from
something that looks pretty to the user -- we want to *parse*.
So we parse into our simple ADT.
Then we turn our simple ADT into our nice GADT.
-
But how?
How do we go from untyped... to typed?
[And in general -- not just into an arbitrary GADT,
but an arbitrary inhabitant of a typeclass.]
[i.e. tagless final, etc]
=
Take 1:
Even if we do not know what type we are creating,
we eventually will do something with it.
So we paramaterize our typechecking function over
an arbitrary continuation.
\begin{code}
mkExpr :: (forall a. (Show a, Typeable a) = Expr a - r) - SimpleExpr -
r
mkExpr k expr = case expr of
SDbl d - k $ EDbl d
SBool b - k $ EBool b
SOpUn op expr1 - case op of
log - k $ mkExpr' (ENumOpUn Log) expr1
exp - k $ mkExpr' (ENumOpUn Exp) expr1
_ - error bad unary op
SOpBi op expr1 expr2 - case op of
add - k $ mkExprBi (ENumOpBi Add) expr1 expr2
sub - k $ mkExprBi (ENumOpBi Sub) expr1 expr2
\end{code}
=
Where's the typechecking?
\begin{code}
mkExpr' k expr = mkExpr (appCast $ k) expr
mkExprBi k expr1 expr2 = mkExpr' (mkExpr' k expr1) expr2
appCast :: forall a b c r. (Typeable a, Typeable b) = (c a - r) - c b -
r
appCast f x = maybe err f $ gcast x
where err = error $ Type error. Expected: ++ show (typeOf
(undefined::a))
++ , Inferred: ++ show (typeOf (undefined::b))
\end{code}
... We let Haskell do all the work!
=
Hmmm... the continuation can be anything.
So let's just make it an existential constructor.
\begin{code}
data ExprBox = forall a. Typeable a = ExprBox (Expr a)
appExprBox :: (forall a. Expr a - res) - ExprBox - res
Re: [Haskell-cafe] Type-Level Programming
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 Bar, you can say Foo 7, where 7 is (of course) a value rather than a type. (?) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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. 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. (?) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Tony Morris http://tmorris.net/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 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 arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. Right. I see. (I think...) Then there are languages like Coq and Agda that support dependent types directly. There you can return a type from a function instead of a value. 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. 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. (FWIW, I have absolutely no clue what that difference is. But if you show me a few Prolog examples, I get the gist of what it does and why that's useful.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 type system (poor Oleg, he's become #haskell's answer to the Chuck Norris meme commonly encountered in MMORPGs). Anyway,... are there any languages out there whose term-level programming resembles Haskell type-level programming, and if so, would a deliberate effort to appeal to that resemblance be an advantage (leaving out for now the hair-pulling effort that such a change would entail)? I'm not a prolog programmer, but I've heard that using type classes to do your computations leads to code that resembles prolog. Indeed. If you like the look of Haskell's type-level programming, you should look at logic programming languages based on Prolog. Datalog gives a well understood fragment of Prolog. ECLiPSe[1] extends Prolog with constraint programming. Mercury[2], lambda-Prolog[3], and Dyna give a more modern take on the paradigm. It's interesting how C++ is imperative at the term level and functional at the type level, while Haskell is functional at the term level and similar to logic programming at the type level. Given imperative, functional, and logic programming, that's nine possible combinations of paradigms at the term and type level. How many of them do we have examples for? imperative/functional: C++ functional/logic: Haskell functional/functional: Agda etc. (?) imperative/imperative: Smalltalk/Ruby? If you're just a fan of logic variables and want something more Haskell-like, there is Curry[4]. In a similar vein there's also AliceML[5] which gives a nice futures/concurrency story to ML. AliceML started out on the same VM as Mozart/Oz[6], which has similar futures, though a different overall programming style. 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. Agda is the most Haskell-like, Epigram draws heavily from the Haskell community, and Coq comes more from the ML tradition. There's a menagerie of others too, once you start looking. [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] http://www-ps.informatik.uni-kiel.de/currywiki/ [5] http://www.ps.uni-saarland.de/alice/ [6] http://www.mozart-oz.org/ -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Work is punishment for failing to procrastinate effectively. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Type-Level Programming
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 program, or to tell character encoding to a program. It is not a programming language issue. If your program saves files using filepaths given by the user or created programatically from another filepath, then you don't need to decode/encode anything and the problem isn't in the programming language. 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 problem we got in Haskell. We have a nice coding-agnostic String datatype, but we don't know how to create a file with this very name. The opposite also may also be problem. Okay, you got an already correctly-encoded filepath. But you want to store this information in your database. Now, you have two options: a) Save the enconded filepath. Each record of your database will potentially have a different encoding, which is very bad. b) Recode into, say, UTF-8. But to do that you need to know the original coding using in the filepath, so we got the same problem above. 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. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Core packages and locale support
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, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 255. and there is no OS except Unix ;) Of course there is, however we should use the least common denominator if we want to create portable programs. Even if other OSs worked fine, should I use this API (i.e. type FilePath = String) to its fullest extent, my program will suddently become unportable to all Unix OSs. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 function
from some type A (which itself is of type Set) and a natural number
(the length) to a new type (of type Set).
The empty list is defined as a zero length vector, and cons therefore
increases the type-level length of the vector by one. Using this
method, Agda can be used to make a fully safe head implementation
that is statically verified not to crash:
head : ∀ { A : Set } { n : ℕ} → Vec A (1 + n) → A
head (x :: xs) = x
This uses the type system to ensure that the vector includes at least
one element.
Note that a similar thing can be achieved in Haskell with the right
extensions, however type-level naturals must be used:
data S n
data Z
data Vec a :: * - * where
Empty :: Vec a 0
Cons :: a - Vec a b - Vec a (S b)
safeHead :: forall b. Vec a (S b) - a
safeHead (Cons x xs) = x
(note: not tested)
The main difference here between Haskell and Agda is that the types
themselves are typed, and that the types contain real naturals not
fake ones like in Haskell
Cheers.
~Liam
On 26 June 2010 22:04, Andrew Coppin andrewcop...@btinternet.com wrote:
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...
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 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 curiosity, what the hell does dependently typed mean anyway? 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 arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. That of course, is only the tip of the iceberg. Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work. Even the example I just gave can be emulated. See this paper: http://www.brics.dk/RS/01/10/ Also SHE: http://personal.cis.strath.ac.uk/~conor/pub/she/ Then there are languages like Coq and Agda that support dependent types directly. There you can return a type from a function instead of a value. I just realized, I may not have made this point sufficiently clear. Much of the reason we need to do extra work in Haskell to emulate dependent types is because types are not first class in Haskell. We can't write terms that manipulate types (type level functions). Instead we use type classes as sets of types and newtypes/data in place of type level functions. But, in dependently typed languages types are first class. Along this line, HList would also serve as a good example of what you would/could do in a dependently type language by showing you how to emulate it in Haskell. Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Core packages and locale support
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 program will suddently become unportable to all Unix OSs. but what you propose cannot be used in Windows at all! while current FilePath still works on Unix, with manual filenames en/decoding -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 program will suddently become unportable to all Unix OSs. 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 back on topic! :) The FilePath datatype is OS-dependent and making it abstract should be at least a first step. If you got it from somewhere else where it is already encoded, then fine. If you need to construct it, then you need to use a smart constructor. If you need to show/print it, then you need to convert it to String. And so on. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 back on topic! :) The FilePath datatype is OS-dependent and making it abstract should be at least a first step. If you got it from somewhere else where it is already encoded, then fine. If you need to construct it, then you need to use a smart constructor. If you need to show/print it, then you need to convert it to String. And so on. 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 problem affect command line arguments and process module. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell Web Framework for newbies?
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 web framework more easy to learn for newbies? Cheers. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 problem affect command line arguments and process module. So that means we should make this change as soon as possible, doesn't it? :) The problem now is designing a future-proof OS-agnostic API to avoid having to change this core part of the base library again in the near future. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
-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, where 7 is (of course) a value rather than a type. (?)
A bit more than that: imagine now that you can (a) replace that 7 with a
variable and (b) do math on it in a type declaration:
-- borrowing 'typevar from ML for a moment...
(SList 'a l) is a sized list of ('a) of length (l)
sListConcat :: SList 'a l1 - SList 'a l2 - SList 'a (l1 + l2)
Just for starters.
- --
brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon university KF8NH
-BEGIN PGP SIGNATURE-
Version: GnuPG v1.4.10 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAkwmD/YACgkQIn7hlCsL25UD8ACghqbV0MUtbfWrFN82yCmsdb4D
X44An2WUkBcuptAe4iz1Wl1t4j3y0NdL
=+6IT
-END PGP SIGNATURE-
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. That of course, is only the tip of the iceberg. That's also a degenerate example, because it doesn't actually require dependent types. What you have here are types dependent on *numbers*, not *values* specifically. That type numbers are rarely built into non-dependently-typed languages is another matter; encoding numbers (inefficiently) as types is mind-numbingly simple in Haskell, not requiring even any exciting GHC extensions (although encoding arithmetic on those numbers will soon pile the extensions on). Furthermore, families of functions of the flavor you describe are doubly degenerate examples: The simplest encoding for type numbers are the good old Peano numerals, expressed as nested type constructors like Z, S Z, S (S Z), and so on... but the arity of a function is *already* expressed as nested type constructors like [b] - ([a] - [(b, a)]), [c] - ([b] - ([a] -[(c,b, a)])), and such! The only complication here is that the zero type changes for each number[0], but in a very practical sense these functions already encode type numbers. Many alleged uses for dependent types are similarly trivial--using them only as a shortcut for doing term-like computations on types. With sufficient sweat, tears, and GHC extensions, most if not all of said degenerate examples can be encoded directly at the type level. For those following along at home, here's a quick cheat-sheet on playing with type programs in GHC: - Type constructors build new type values - Type classes in general associate types with term values inhabiting them - Type families and MPTCs with fundeps provide functions on types - When an instance is selected, everything in its context is evaluated - Instance selection that depends on the result of another type function provides a sort of lazy evaluation (useful for control structures) - Getting anything interesting done usually needs UndecidableInstances plus Oleg's TypeEq and TypeCast classes Standard polymorphism also involves functions on types in a sense, but doesn't allow computation on them. As a crude analogy, one could think of type classes as allowing pattern matching on types, whereas parametric polymorphism can only bind types to generic variables without inspecting constructors. Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work. Encoding *actual* instances of dependent types in some fashion is indeed possible, but it's a bit trickier. The examples you cite deal largely with making the degenerate cases more pleasant to work with; the paper by a charming bit of Church-ish encoding that weaves the desired number-indexed function right into the definition of the zero and successor, and she... well, she's a sight to behold to be sure, but at the end of the day she's not really doing all that much either. Since any value knowable at compile-time can be lifted to the type level one way or another, non-trivial faux-dependent types must depend on values not known until run-time--which of course means that the exact type will be unknown until run-time as well, i.e., an existential type. For instance, Oleg's uses of existential types to provide static guarantees about some property of run-time values[1] can usually be reinterpreted as a rather roundabout way of replicating something most naturally expressed by actual dependent types. Which isn't to say that type-level programming isn't useful, of course--just that if you know the actual type at compile-time, you don't really need dependent types. - C. [0] This is largely because of how Haskell handles tuples--the result of a zipN function is actually another type number, not a zero, but there's no simple way to find the successor of a tuple. More sensible, from a number types perspective, would be to construct tuples using () as zero and (_, n) as successor. This would give us zip0 :: [()], zip1 :: [a] - [(a, ())], zip2 :: [b] - ([a] - [(b, (a, ()))]), and so on. The liftM and zipWith functions avoid this issue. [1] See http://okmij.org/ftp/Haskell/types.html#branding and http://okmij.org/ftp/Haskell/regions.html for instance. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 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 expression is equivalent to Haskell's bottom type a. Indeed, Haskell is a weak second-order language. Haskell's language of values, functions, and function application is a first- order language. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Space leak with unsafePerformIO
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 program writes a file to the disk until it is full. Any idea?
The original problem is a function that is compiled by LLVM and shall be
applied to a list in a mapAccumL manner.
{-
$ ghc --make -Wall -O -prof -auto-all InterleaveIO.hs
$ InterleaveIO +RTS -M1m -prof-all -RTS
-}
import System.IO.Unsafe (unsafePerformIO, unsafeInterleaveIO, )
makeSuccUnsafe1 :: IO ([Char] - [Char])
makeSuccUnsafe1 =
return $
\ sig - unsafePerformIO $ do
let go xt =
unsafeInterleaveIO $
case xt of
[] - return []
x:xs - fmap (succ x :) $ go xs
go sig
makeSuccUnsafe :: IO ([Char] - [Char])
makeSuccUnsafe =
return $
\ sig -
let go xt =
unsafePerformIO $
case xt of
[] - return []
x:xs - return (succ x : go xs)
in go sig
makeSuccPlain :: IO ([Char] - [Char])
makeSuccPlain =
return $
\ sig -
let go xt =
case xt of
[] - []
x:xs - succ x : go xs
in go sig
splitAtLazy :: [b] - [a] - ([a],[a])
splitAtLazy nt xt =
(\ ~(ys,zs) - (ys,zs)) $
case (nt,xt) of
(_:ns, x:xs) -
let (ys,zs) = splitAtLazy ns xs
in (x:ys,zs)
(_, xs) - ([],xs)
makeTwoLists :: Char - ([Char], [Char])
makeTwoLists c =
splitAtLazy (repeat ()) $ repeat c
main :: IO ()
main = do
succUnsafe - makeSuccUnsafe
succPlain - makeSuccPlain
writeFile test.txt $
let (prefix, suffix) = makeTwoLists 'a'
in case 3::Int of
-- no leak
0 - succUnsafe $ prefix ++ suffix
-- no leak
1 - succPlain $ prefix ++ suffix
-- no leak
2 - succPlain prefix ++ succPlain suffix
-- leak
3 - succUnsafe prefix ++ succPlain suffix
-- no leak
4 - succPlain prefix ++ succUnsafe suffix
-- leak
5 - succUnsafe prefix ++ succUnsafe suffix
_ - error not implemented
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Huffman Codes in Haskell
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) deriving Show bfnum :: Tree a - Tree Int bfnum = num . bf bf :: Tree a - [Tree a] bf root = output where children = go 1 output output = root : children go 0 _ = [] go n (E : rest) = go (pred n) rest go n (T _ a b : rest) = a : b : go (succ n) rest num :: [Tree a] - Tree Int num input = root where root : children = go 1 input children go k (E : input) children = E : go k input children go k (T _ _ _ : input) ~(a : ~(b : children)) = T k a b : go (succ k) input children Maybe one could try to fuse bf and num. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 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 expression is equivalent to Haskell's bottom type a. Indeed, Haskell is a weak second-order language. Haskell's language of values, functions, and function application is a first-order language. I have literally no idea what you just said. It's like, I have C. J. Date on the shelf, and the whole chapter on the Relational Calculus just made absolutely no sense to me because I don't understand the vocabulary. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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: imagine now that you can (a) replace that 7 with a variable and (b) do math on it in a type declaration. Right, I see. So is there a specific reason why Haskell isn't dependently typed then? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Emacs script to align Haskell import list
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 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 provide a simple revision history and comment support. Please feel free to contribute some tweaks and fixes. I'll then see about merging this into haskell-mode in some fashion. It doesn't handle multiple line explicit imports as I have a personal rule that any explicit import list with more than a few symbols should be changed to an as X import, as an addition to tibbe's style guide.[1] I haven't decided on a recommended keybinding. I'm considering a context-dependent binding of C-c C-. that indents the import list when you are on an import line. [1]: http://github.com/tibbe/haskell-style-guide ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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, where 7 is (of course) a value rather than a type. (?) A bit more than that: imagine now that you can (a) replace that 7 with a variable and (b) do math on it in a type declaration. Right, I see. So is there a specific reason why Haskell isn't dependently typed then? Or you could ask, So is there a specific reason why C isn't a functional language? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 expression is equivalent to Haskell's bottom type a. Indeed, Haskell is a weak second-order language. Haskell's language of values, functions, and function application is a first-order language. I have literally no idea what you just said. It's like, I have C. J. Date on the shelf, and the whole chapter on the Relational Calculus just made absolutely no sense to me because I don't understand the vocabulary. Let's break it down then. A language is a set of terms or expressions, together with rules for putting terms together (resulting in sentences, in the logic vocabulary). A logic is a language with rules of inference that let you transform sets of sentences into new sentences. Quantification is a tricky thing to describe. In short, if a language can quantify over something, it means that you can have variables of that kind. So, Haskell can quantify over integers, since we can have variables like x :: Integer. More generally, Haskell's run- time language quantifies over values. From this point of view, Haskell is TWO languages that interact nicely (or rather, a second-order language). First, there is the term-level run-time language. This is the stuff that gets evaluated when you actually run a program. It can quantify over values and functions. And we can express function application (a rule of inference to combine a function and a value, resulting in a new value). Second, there is the type language, which relies on specific keywords: data, class, instance, newtype, type, (::) Using these keywords, we can quantify over types. That is, the constructs they enable take types as variables. However, notice that a type is really a collection of values. For example, as the Gentle Introduction to Haskell says, we should think of the type Integer as being: data Integer = 0 | 1 | -1 | 2 | -2 | ... despite the fact that this isn't how it's really implemented. The Integer type is just an enumeration of the integers. Putting this all together and generalizing a bit, a second-order language is a language with two distinct, unmixable kinds variables, where one kind of variable represents a collection of things that can fill in the other kind of variable. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
-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 (a) replace that 7 with a variable and (b) do math on it in a type declaration. So is there a specific reason why Haskell isn't dependently typed then? Or you could ask, So is there a specific reason why C isn't a functional language? More to the point, Haskell was a bit too frozen in stone when dependent type theory reached the point of being implementable. As a case in point, you'll notice in my sized-list example in pseudo-Haskell I had to drag in syntax from ML to distinguish type variables from value variables? Hard to escape that with Haskell as it currently exists --- but in a proper dependently typed system, there is no such distinction: types aren't different kinds of things from values. (Or in the usual lingo, types are first class values in dependently-typed languages.) Compare my example to the Agda example someone else posted; Agda is a proper dependently typed language, and the value and type variables are treated exactly the same way. - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkwmcEgACgkQIn7hlCsL25UaRgCgybBPBhtn2evzDA6+0D9L3uph XVsAni86B2NDPZPCPvIc1Us53rj3hh06 =LxLd -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 -- -- Erik de Castro Lopo http://www.mega-nerd.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 simply-typed λ-calculus, but the best you can do beyond that is probably the Damas/Hindley/Milner algorithm which covers a (rather useful) subset of System F. This is the heart of Haskell's type inference, but some GHC extensions make type inference undecidable, such as RankNTypes. Type inference being undecidable is only a problem insofar as it requires adding explicit type annotations until the remaining types can be inferred. - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 manual filenames en/decoding Now we got back on topic! :) The FilePath datatype is OS-dependent and making it abstract should be at least a first step. If you got it from somewhere else where it is already encoded, then fine. If you need to construct it, then you need to use a smart constructor. If you need to show/print it, then you need to convert it to String. And so on. 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. I fail to see how it will brake programs. Current programs do not use Unicode because it is implemented incorrectly. -- Best regards, Roman Beslik. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 mount options. No need to change a program, or to tell character encoding to a program. It is not a programming language issue. If your program saves files using filepaths given by the user or created programatically from another filepath, then you don't need to decode/encode anything and the problem isn't in the programming language. 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 problem we got in Haskell. We have a nice coding-agnostic String datatype, but we don't know how to create a file with this very name. It is simple — you recode from (database | network server | file) encoding to the current locale. -- Best regards, Roman Beslik. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 problem we got in Haskell. We have a nice coding-agnostic String datatype, but we don't know how to create a file with this very name. It is simple — you recode from (database | network server | file) encoding to the current locale. Recoding is indeed very simple. You know the source coding (e.g. your database is in UTF-8). But how do you discover the target coding? How can you find out that this system uses ISO8859-1, while this other one uses UTF-16, while...? See the problem now? :) Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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 Windows at all! while current FilePath still works on Unix, with manual filenames en/decoding Now we got back on topic! :) The FilePath datatype is OS-dependent and making it abstract should be at least a first step. If you got it from somewhere else where it is already encoded, then fine. If you need to construct it, then you need to use a smart constructor. If you need to show/print it, then you need to convert it to String. And so on. 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. I fail to see how it will brake programs. Current programs do not use Unicode because it is implemented incorrectly. For example, this program would break: import System.Environment (getArgs) main :: IO () main = getArgs = \[a] - writeFile a hello world The types are: getArgs :: IO [String] writeFile :: FilePath - String - IO () Right now we have type FilePath = String so the code above works. If we had data FilePath = ... then that would be a type error work at all. So even one of the most trivial programs wouldn't compile anymore. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
-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 programs because there is no constructor for FilePath currently, so everyone uses String. And Haskell doesn't auto-coerce, so you would need to use a typeclass and separate String and FilePath instances for compatibility. (On the other hand, this might be a good idea anyway; another instance that would be useful would be [Word8].) - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkwmpGgACgkQIn7hlCsL25W4IACdEzcDMkz62yqn4wKfx49y0zXy DRcAnjxWf0a4SdBE7lBLVFZessUeVJ+n =XreM -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Core packages and locale support
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) getArgs :: IO [FilePath] d) getArgs :: IO [Argument] Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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] http://www-ps.informatik.uni-kiel.de/currywiki/ [5] http://www.ps.uni-saarland.de/alice/ [6] http://www.mozart-oz.org/ Are any of those compatible with Haskell, so that we could mix code in that language with Haskell code? Your best bets would be Agda and Curry. I'm not familiar enough with either of them to know what sort of FFI or cross-linking they support, but both are (by design) rather similar to Haskell. For Curry, it may also vary depending on the compiler. With all the others, interaction will be restricted to generic FFI support. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 type) Hmm. This sounds like one of those things where the idea is simple, but the consequences are profound... The simplest fully[1] dependently typed formalism is one of the many variants of LF. LF is an extension of the simply typed lambda calculus, extending the arrow type constructor to be ((x:a) - b) where the variable x is bound to the argument value and has scope over b. In order to make use of this, we also allow type constructors with dependent kinds, for example with the type family (P : A - *) we could have a function (f : (x:A) - P x). Via Curry--Howard isomorphism this gives us first-order intuitionistic predicate calculus (whereas STLC is 1st-order propositional calculus). The switch from atomic propositions to predicates is where the profundity lies. A common extension to LF is to add dependent pairs, generalizing the product type constructor to be ((x:a) * b), where the variable x is bound to the first component of the pair and has scope over b. This extension is rather trivial in the LF setting, but it can cause unforeseen complications in more complex formalisms. Adding dependencies is orthogonal to adding polymorphism or to adding higher-orderness. Though orthogonal should probably be said with scare-quotes. In the PTS presentation of Barendregt's lambda cube these three axes are indeed syntactically orthogonal. However, in terms of formal power, the lambda cube isn't really a cube as such. There are numerous shortcuts and wormholes connecting far reaches in obscure non-Euclidean ways. The cube gives a nice overview to start from, but don't confuse the map for the territory. One particular limitation of LF worth highlighting is that, even though term-level values may *occur* in types, they may not themselves *be* types. That is, in LF, we can't have any function like (g : (x:a) - x). In the Calculus of Constructions (CC)[2], this restriction is lifted in certain ways, and that's when the distinction between term-level and type-level really breaks down. Most current dependently typed languages (Coq, Agda, Epigram, LEGO, NuPRL) are playing around somewhere near here, whereas older languages tended to play around closer to LF or ITT (e.g., Twelf). And as a final note, GADTs and type families are forms of dependent types, so GHC Haskell is indeed a dependently typed language (of sorts). They're somewhat kludgy in Haskell because of the way they require code duplication for term-level and type-level definitions of the same function. In real dependently typed languages it'd be cleaner to work with these abstractions since we could pass terms into the type level directly, however that cleanliness comes with other burdens such as requiring that all functions be provably terminating. Managing to balance cleanliness and the requirements of type checking is an ongoing research area. (Unless you take the Cayenne route and just stop caring about whether type checking will terminate :) [1] Just as Hindley--Milner is an interesting stopping point between STLC and System F, there are also systems between STLC and LF. [2] In terms of formal power: CC == F_omega + LF == ITT + SystemF. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-Level Programming
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 with--- er, reading the documentation for languages like Coq, is that the class of problems which motivate the need to move to such powerful formalisms are often so abstract that it is hard to come up with simple practical examples of why anyone should care. There are examples everywhere, but complex machinery is only motivated by complex problems, so it's hard to find nice simple examples. In particular, I've noticed that once you start *using* Coq (et al.) and trying to prove theorems about your programs, the subtle issues that motivate the complex machinery begin to make sense. For example, there's a lot of debate over whether Axiom K is a good thing or not. Just reading the literature doesn't shed any light on the real ramifications of having the axiom vs not; you really need to go about trying to prove definitional equalities and seeing the places where you can't proceed without it, before you can appreciate what all the hubbub is about. 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. (FWIW, I have absolutely no clue what that difference is. First-order means you can only quantify over simple things. Second-order means you can also quantify over quantification, as it were. For example, the type system of simply-typed lambda calculus is 1st-order intuitionistic propositional logic, and System F (i.e., STLC + rank-n polymorphism) is 2nd-order. (F_omega is higher-order, but that's one of those wormholes in the lambda cube.) Though higher-order is a much abused term, which may cause some of the confusion. The higher-orderness discussed above has to do with quantification within types, which has to do with higher-orderness of the related logics. But we can also talk about a different sort of higher-orderness, namely what distinguishes System F from F_omega, or distinguishes LF from ITT. In STLC we add a simple language of types at a layer above the term layer, in order to make sure the term layer behaves itself. After hacking around we eventually decide it'd be cool to have functions at the type level. But how to we make sure that our types are well-formed? Well, we add a new layer of simple types on top of the type layer--- which gives us a second-order system. We could repeat the process again once we decide we want kind-level functions too.[1] To take a different track, in cognitive science people talk about theory of mind, i.e. the idea that we each theorize that other people have minds, desires, beliefs, etc. A first-order theory of mind is when we attribute a mind to other people. A second-order theory of mind is when we attribute a theory of mind to other people (i.e., we believe that they believe that we have a mind). Etc. In epistemic/doxastic logics we can talk about first-order knowledge/beliefs, that is beliefs in simple propositions. But we can also talk about second-order beliefs, that is beliefs about beliefs. Etc. [1] See Tim Sheard's Omega for the logical conclusion of this process. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
