Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?
Hi, Ryan Newton wrote: It is very hard for me to see why people should be able to make their own Generic instances (that might lie about the structure of the type), in Safe-Haskell. I guess that lying Generics instances might arise because of software evolution. Let's say we start with an abstract data type of binary trees. module Tree (Tree, node, empty, null, split) where data Tree a = Node (Tree a) (Tree a) | Empty deriving Generics node = Node empty = Empty null Empty = True null _ = False split (Node a b) = (a, b) size Empty = 0 size (Node x y) = size x + size y Note that this data type is not really abstract, because we export the Generics instance, so clients of this module can learn about the implementation of Tree. This is not a big deal, because the chosen implementation happens to correspond to the abstract structure of binary trees anyway. So I would expect that generic code will work fine. For example, you could use generic read and show functions to serialize trees, and get a reasonable data format. Now, we want to evolve our module by caching the size of trees. We do something like this: module Tree (Tree, node, empty, null, split) where data Tree a = Tree !Int (RealTree a) data RealTree a = Node (Tree a) (Tree a) | Empty tree (Node a b) = Tree (size a + size b) t tree Empty = Tree 0 Empty node x y = tree (Node x y) empty = tree Empty null (Tree _ Empty) = True null _ = False split (Tree _ (Node a b)) = (a, b) size (Tree n _) = n Except for the Generics instance, we provide the exact same interface and behavior to our clients, we just traded some space for performance. But what Generics instance should we provide? If we just add deriving Generics to the two datatypes, we leak the change of representation to our clients. For example, a client that serialized a tree with a generic show function based on the old Tree cannot hope to deserialize it back with a generic read function based on the new Tree. The size information would be missing, and the structure would be different. If we write a Generics instance by hand, however, I guess we can make it present the exact same structure as the derived Generics instance for the old Tree. With this lying instance, the generic read function will happily deserialize the old data. The size will be computed on the fly, because our hand-written Generics instance will introduce calls to our smart constructors. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Any precedent or plan for guaranteed-safe Eq and Ord instances?
Hi, Roman Cheplyaka wrote: It still seems to fit nicely into Safe Haskell. If you are the implementor of an abstract type, you can do whatever you want in the Eq instance, declare your module as Trustworthy, and thus take the responsibility for soundness of that instance w.r.t. your public API. A possible problem with marking instance Eq as an unsafe feature is that many modules would be only Trustworthy instead of Safe. So if I don't trust the authors of a module (because I don't know them), I cannot safely use their code just because they implement their own Eq instance? That would go against my every purely functional module is automatically safe because the compiler checks that it cannot launch the missiles understanding of Safe Haskell. Actually, Eq instances are not unsafe per se, but only if I also use some other module that assumes certain properties about all Eq instances in scope. So in order to check safety, two independent modules (the provider and the consumer of the Eq instance) would have to cooperate. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why isn't hsc2hs functionality provided by ghc?
Hi, Roman Cheplyaka wrote: My preferred solution would be to have ghc/ghci automatically run hsc2hs [...] when necessary. How about having a `ghci` command for cabal? I don't think cabal can provide that. Let's say you're inside a 'cabal ghci' session. If you modify the hsc file and reload it in ghci, you'd expect to load the updated version — yet cabal hasn't even been called since 'cabal ghci', and have had no chance to re-generate the hs file. Maybe ghci could be changed to call some kind of hook everytime a file is called, and cabal could then provide an implementation for this hook that regenerates the files if necessary? Maybe this is even possible today using: :def r somethingCleverHere A quick test shows some minor problems, like :def r (const (return :r)) :r looping. But maybe this could be figured out. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADT and instance deriving
Hi,
TP wrote:
Today I have a type constructor Tensor in which there is a data
constructor Tensor (among others):
data Tensor :: Nat - * where
[...]
Tensor :: String - [IndependentVar] - Tensor order
[...]
The idea is that, for example, I may have a vector function of time and
position, for example the electric field:
E( r, t )
(E: electric field, r: position vector, t: time)
So, I have a Tensor (E) that depends on two tensors (r and t). I want to put
r and t in a list, the list of independent variable of which E is a
function. But we see immediately that r and t have not the same type: the
first is of type Tensor One, the second of type Tensor Zero. Thus we
cannot put them in a list.
I don't know what a tensor is, but maybe you have to track *statically*
what independent variables a tensor is a function of, using something like:
E :: R - T - Tensor ...
or
E :: Tensor (One - Zero - ...)
or
E :: Tensor '[One, Zero] ...
I have two simple pointers to situations where something similar is
going on. First, see the example for type-level lists in the GHC user's
guide:
http://www.haskell.org/ghc/docs/latest/html/users_guide/promotion.html#promoted-lists-and-tuples
data HList :: [*] - * where
HNil :: HList '[]
HCons :: a - HList t - HList (a ': t)
In this example, an HList is an heterogenous list, but it doesn't use
existential types. Instead, we know statically what the types of the
list elements are, because we have a type-level list of these element types.
And the second situation: The need for such type-level lists also shows
up when you try to encode well-typed lambda terms as a datatype. You
have to reason about the free variables in the term and their type. For
example, the constructor for lambda expressions should remove one free
variable from the term. You can encode this approximately as follows:
data Type = Fun Type Type | Num
data Term :: [Type] - Type - * where
-- arithmetics
Zero :: Term ctx 'Num
Succ :: Term ctx 'Num - Term ctx 'Num
Add :: Term ctx 'Num - Term ctx 'Num - Term ctx 'Num
-- lambda calculus
App :: Term ctx ('Fun a b) - Term ctx a - Term ctx b
Lam :: Term (a ': ctx) b - Term ctx ('Fun a b)
Var :: Var ctx a - Term ctx a
-- variables
data Var :: [Type] - Type - * where
This :: Var (a ': ctx) a
That :: Var ctx a - Var (b ': ctx) a
The point is: We know statically what free variables a term can contain,
similarly to how you might want to know statically the independent
variables of your tensor.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] rip in the class-abstraction continuum
Hi,
Christopher Howard wrote:
class XyConv a where
toXy :: a b - [Xy b]
[...]
I can get a quick fix by adding Floating to the context of the /class/
definition:
class XyConv a where
toXy :: Floating b = a b - [Xy b]
But what I really want is to put Floating in the context of the
/instance/ declaration.
This is not easily possible. If you could just put the constraint into
the instance, there would be a problem when youc all toXy in a
polymorphic context, where a is not known. Example:
class XyConv a where
toXy :: a b - [Xy b]
shouldBeFine :: XyConv a = a String - [Xy String]
shouldBeFine = toXy
This code compiles fine, because the type of shouldBeFine is an instance
of the type of toXy. The type checker figures out that here, b needs to
be String, and since there is no class constraint visible anywhere that
suggests a problem with b = String, the code is accepted.
The correctness of this reasoning relies on the fact that whatever
instances you add in other parts of your program, they can never
constrain b so that it cannot be String anymore. Such an instance would
invalidate the above program, but that would be unfair: How would the
type checker have known in advance whether or not you'll eventually
write this constraining instance.
So this is why in Haskell, the type of a method in an instance
declaration has to be as general as the declared type of that method in
the corresponding class declaration.
Now, there is a way out using some of the more recent additions to the
language: You can declare, in the class, that each instance can choose
its own constraints for b. This is possible by combining constraint
kinds and associated type families.
{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
import GHC.Exts
The idea is to add a constraint type to the class declaration:
class XyConv a where
type C a :: * - Constraint
toXy :: C a b = a b - [Xy b]
Now it is clear to the type checker that calling toXy requires that b
satisfies a constraint that is only known when a is known, so the
following is not accepted.
noLongerAccepted :: XyConv a = a String - [Xy String]
noLongerAccepted = toXy
The type checker complains that it cannot deduce an instance of (C a
[Char]) from (XyConv a). If you want to write this function, you have to
explicitly state that the caller has to provide the (C a String)
instance, whatever (C a) will be:
haveToWriteThis :: (XyConv a, C a String) = a String - [Xy String]
haveToWriteThis = toXy
So with associated type families and constraint kinds, the class
declaration can explicitly say that instances can require constraints.
The type checker will then be aware of it, and require appropriate
instances of as-yet-unknown classes to be available. I think this is
extremely cool and powerful, but maybe more often than not, we don't
actually need this power, and can provide a less generic but much
simpler API.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
Hi, Patrick Browne wrote: In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. Yes. Haskell function definitions look like equations, but in many ways, they aren't. Here is an example for an equation that is not valid as a Haskell function definition: g x = 42 f (g x) = x-- not valid The problem is that we cannot use g at the left-hand side. Here is an example that doesn't mean what you might be hoping for: f x = f x f x = 42 Seen as an equation system, this should constrain f to be a function that always returns 42. But in Haskell, it defines f to be a non-terminating function. The reason is that only the first line counts, because it covers all possible argument values. The second line is ignored. The behavior changes if we swap the two lines: g x = 42 g x = g x Again, only the first line counts, so g is the function that always returns 42. Here is a more complicated example: h 27 = 42 h x = h x h 13 = 100 What function is h? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hackage checking maintainership of packages
Hi, Petr Pudlák wrote: -- Forwarded message -- From: *Niklas Hambüchen* m...@nh2.me mailto:m...@nh2.me Date: 2013/5/4 ... I would even be happy with newhackage sending every package maintainer a quarterly question Would you still call your project X 'maintained'? for each package they maintain; Hackage could really give us better indications concerning this. This sounds to me like a very good idea. It could be as simple as If you consider yourself to be the maintainer of package X please just hit reply and send. If Hackage doesn't get an answer, it'd just would display some red text like This package seems to be unmaintained since D.M.Y. I like the idea of displaying additional info about the status of package development, but I don't like the idea of annoying hard-working package maintainers with emails about their perfect packages that actually didn't need any updates since ages ago. So what about this: Hackage could try to automatically collect and display information about the development status of packages that allow potential users to *guess* whether the package is maintained or not. Currently, potential users have to collect this information themselves. Here are some examples I have in mind: * Fetch the timestamp of the latest commit from the HEAD repo * Fetch the number of open issues from the issue tracker * Display reverse dependencies on the main hackage page * Show the timestamp of the last Hackage upload of the uploader Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hackage checking maintainership of packages
Hi, Niklas Hambüchen wrote: Having the metrics you mention is nice, but still they are just metrics and say little the only thing that's important: Is there a human who commits themselves to this package? I like the idea of displaying additional info about the status of package development, but I don't like the idea of annoying hard-working package maintainers with emails about their perfect packages I really think this is not too big of a deal, getting one email every 3 months and clicking a few checkboxes. Is a human clicked the check box a good metric for a human commits themselves to this package? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Prolog-style patterns
Hi, Jan Stolarek wrote: If Haskell allowed to write pattern matching similar to Prolog then we could write this function like this: member :: Eq a = a - [a] - Bool member _ [] = False member x (x:_) = True member x (_:xs) = member x xs The meaning of pattern in the second equation is match this equation if the first argument equals to head of the list. You can achieve something similar with the ViewPatterns language extension. See http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#view-patterns and http://hackage.haskell.org/trac/ghc/wiki/ViewPatterns. member _ [] = False member x (((x ==) - True) : _) = True member x (_ : xs) = member x xs or member _ [] = False member x ((compare x - EQ) : _) = True member x (_ : xs) = member x xs Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is there an escape from MonadState+MonadIO+MonadError monad stack?
Hi, Ömer Sinan Ağacan wrote: One thing I'm not happy about my Haskell programs is, almost all of my programs have a monad transformer stack consisting MonadError, MonadIO and MonadState. You can try to write most of your program in pure functions that are called from a few main functions in the monad. Or, if you need some but not all monadic actions in each function, you can use the following pattern: -- This helper function cannot cause monadic effects other than -- throwing errors. But it can be used in arbitrary monads that -- support throwing errors. helper :: MonadError MyError m = ... - m ... helper = do ... -- Same but with only allowing IO, but other monadic actions other :: MonadIO m = ... - m ... other = do ... -- we can use both functions in the same monad main = runMyStack $ do helper other This way, you have some control over what effects are allowed where. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
Hi,
Richard A. O'Keefe wrote:
As I understand it, in ML, it seemed to be a clever idea to not have type
signatures at all.
Wrong. In ML, it seemed to be a clever idea not to *NEED* type signatures,
and for local definitions they are very commonly omitted.
In the ML I used, I remember that it was syntactically impossible to use
type signatures directly adjacent to a local definition. Instead, I was
thaught to put something like a type signature in a comment,
approximately like this:
(* getOpt : 'a option * 'a - 'a *)
fun getOpt (SOME x, y) = x
| getOpt (NONE, y) = y
An example of this style can be found in Danvy and Nielsen,
Defunctionalization at Work, Proc. of PPDP 2001 (extended version
available at
ftp://ftp.daimi.au.dk/pub/BRICS/Reports/RS/01/23/BRICS-RS-01-23.pdf).
But you can certainly HAVE type signatures, and for modules
('structures') it is normal to have them in the interfaces ('signatures').
In my opinion, a signature for a structure would not count as directly
adjacent. Also, while I don't know much about the history of ML, I
suspect that structures and signatures were a later addition to the core
language.
I just checked Milner, Tofte and Harper, The Definition of Standard ML,
MIT Press 1990 (available at
http://www.itu.dk/people/tofte/publ/1990sml/1990sml.html), and learned
that we can have explicit type annotations for both patterns and
expressions, so the following variants of the above are possible in
Standard ML:
1. We can embed parts of the signature into the definition:
fun getOpt (SOME (x : 'a), y : 'a) : 'a = x
| getOpt (NONE, y : 'a) : 'a = y
With decomposing the type signature into its parts, and then duplicating
these parts, this is not very attractive.
2. We can do better by avoiding the derived form for function bindings:
val getOpt : 'a option * 'a - 'a
= fn (SOME x, y) = x
| (NONE, y) = y
This looks ok to me, and I wonder why I was not thaught this style, at
least as an alternative. The benefit over type signatures in comments is
clear: The type checker will check that the signatures are accurate, and
there is a chance that error messages contain type variables chosen by
the programmer instead of automatically generated names.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: antiquoter-0.1.0.0
Hi, L Corbijn wrote: I'm happy to announce the release of my first package antiquoter, a combinator library for writing quasiquoters and antiquoters. The main aim is to simplify their definitions and reduce copy-and-paste programming. Very interesting. I'm using something similar to your EP class, but yours looks more refined. See class PatOrExp in https://github.com/Toxaris/pts/blob/master/src-lib/PTS/QuasiQuote.hs I'm a bit overwhelmed by the rest of your library, though. Is the overall design explained somewhere? And: Your package description says that it is especially aimed at making user extensible antiquoters. That sounds very cool. Can you provide an example for how the antiquoter package supports extensions, and what kinds of extensions are supported? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
Hi Johannes, Johannes Waldmann wrote: I absolutely dislike it when I have to jump through hoops to declare types in the most correct way, and in the most natural places. reverse :: forall (a :: *) . [a] - [a] \ (xs :: [Bool]) - ... All of this just because it seemed, at some time, a clever idea to allow the programmer to omit quantifiers? As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all. From the type-theoretic point of view, I guess this is related to your view of what a polymorphic function is. One view says that a polymorphic function is qualitatively different from each of its instances and that forall is a type constructor, so there should be introduction and elimination forms for terms of that type. Instantiation and generalization are explicit operations with computational content, that is, they have some effect at runtime. This view leads to System F with its explicit type abstraction and type application forms. The other view says that a polymorphic function is the union of all of its instances and that instantation and generalization are implicit, structural operations that have no computational content, that is, they do not affect what happens at runtime. This view leads to ML with its very implicit handling of polymorphism. It seems that in Haskell, we started with the ML-ish view that polymorphism is an implicit, structural thing, but we moved further and further towards the System-F-ish view that polymorphism is an explicit, computational thing. A good indicator for this is the Monomorphism restriction, which supposedly helps beginners to cope with the computational effects of polymorphism. So apparently, there *are* such effects. Another indicator is the type classes in that they attach further computational content with type variables. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.
Hi Kim-Ee, Kim-Ee Yeoh wrote: [...] I guess this is related to your view of [...] Do you have a reference to the previous conversation? Sorry, I mean related to one's view of, not related to Johannes Waldmanns' view of. Which seems miles away from what you're alluding to. Full-blown type-level programming? Operational semantics at the type-level? I'm not sure. That's not what I tried to allude to. I mean the operational semantics of instantiation and generalization *at the term level*. In System F, there are two contraction rules: The usual β rule (λx : τ . e1) e2 ~ subst e2 for x in e1 and an additional β-like rule for type application and abstraction: (Λα . e) [τ] ~ subst τ for α in e So in System F, type application and type abstraction have computational content. I think this can become visible in GHC Haskell as well, but I cannot find an example without type classes. Maybe I'm wrong. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Conflicting bindings legal?!
Hi,
Andreas Abel wrote:
To your amusement, I found the following in the Agda source:
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x = do
scope - getScope
let scope' = scope { scopePrecedence = ctx }
return $ abstractToConcrete (makeEnv scope') x
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
I am surprised this is a legal form of shadowing. To understand which
definition of 'scope' shadows the other, I have to consult the formal
definition of Haskell.
Isn't this just an instance of the following, more general rule:
To understand what a piece of code means, I have to consult the formal
definition of the language the code is written in.
In the case you cite, you just have to desugar the do notation
abstractToConcreteCtx :: ToConcrete a c = Precedence - a - TCM c
abstractToConcreteCtx ctx x =
getScope = (\scope -
let scope' = scope { scopePrecedence = ctx } in
return $ abstractToConcrete (makeEnv scope') x)
where
scope = (currentScope defaultEnv) { scopePrecedence = ctx }
and it becomes clear by the nesting structure that the lambda-binding
shadows the where-binding. It seems that if you argue against this case,
you argue against shadowing in general. Should we adopt the Barendregt
convention as a style guide for programming?
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
Hi Martin, Martin Drautzburg wrote: Note that the left recursion is already visible in the grammar above, no need to convert to parser combinators. The problem is that the nonterminal Exp occurs at the left of a rule for itself. Just a silly quick question: why isn't right-recursion a similar problem? I think the situation is symmetric: If you match the token stream right-to-left, right-recursion is problematic. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
Hi, Kim-Ee Yeoh wrote: Perhaps you meant /productive/ corecursion? Because the definition A ::= B A you gave is codata. If you write a recursive descent parser, it takes the token stream as an input and consumes some of this input. For example, the parser could return an integer that says how many tokens it consumed: parseA :: String - Maybe Int parseB :: String - Maybe Int Now, if we implement parseA according to the grammar rule A ::= B A we have, for example, the following: parseA text = case parseB text of Nothing - Nothing Just n1 - case parseA (drop n1 text) of Nothing - Nothing Just n2 - Just (n1 + n2) Note that parseA is recursive. The recursion is well-founded if (drop n1 text) is smaller then text. So we have two cases, as Roman wrote: If the language defined by B contains the empty string, then n1 can be 0, so the recursion is not well-founded and the parser might loop. If the language defined by B does not contain the empty string, then n1 is always bigger than 0, so (drop n1 text) is always smaller than text, so the recursion is well-founded and the parser cannot loop. So I believe the key to understanding Roman's remark about well-founded recursion is to consider the token stream as an additional argument to the parser. However, the difference between hidden left recursion and unproblematic recursion in grammars can also be understood in terms of productive corecursion. In that view, a parser is a process that can request input tokens from the token stream: data Parser = Input (Char - Parser) | Success | Failure parseA :: Parser parseB :: Parser Now, if we implement parseA according to the grammar rule A ::= B A we have, for example, the following: andThen :: Parser - Parser - Parser andThen (Input f) p = Input (\c - f c `andThen` p) andThen (Success) p = p andThen Failure p = p parseA = parseB `andThen` parseA Note that parseA is corecursive. The corecursion is productive if the corecursive call to parseA is guarded with an Input constructor. Again, there are two cases: If the language described by B contains the empty word, then parseB = Success, and (parseB `andThen` parseA) = parseA, so the corecursive call to parseA is not guarded and the parser is not productive. If the langauge described by B does not contain the empty word, then parseB = Input ..., and (parseB `andThen` parseA) = Input (... parseA ...), so the corecursive call to parseA is guarded and the parse is productive. So I believe the key to understanding left recursion via productive corecursion is to model the consumption of the token stream with a codata constructor. Both approaches are essentially equivalent, of course: Before considering the very same nonterminal again, we should have consumed at least one token. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
Hi, Martin Drautzburg wrote: As an exercise I am writing a parser roughly following the expamples in Graham Hutton's book. The language contains things like: data Exp = Lit Int -- literal integer | Plus Exp Exp So the grammar is: Exp ::= Int | Exp + Exp My naive parser enters an infinite recursion, when I try to parse 1+2. I do understand why: hmm, this expression could be a plus, but then it must start with an expression, lets check. and it tries to parse expression again and again considers Plus. Indeed. Twan van Laarhoven told me that: Left-recursion is always a problem for recursive-descend parsers. Note that the left recursion is already visible in the grammar above, no need to convert to parser combinators. The problem is that the nonterminal Exp occurs at the left of a rule for itself. One way to fix this problem is to refactor the grammar in order to avoid left recursion. So let's distinguish expressions that can start with expressions and expressions that cannot start with expressions: Exp-norec ::= Int Exp-rec ::= Exp-norec | Exp-norec + Exp-rec Note that Exp-rec describes a list of Exp-norec with + in-between, so you can implement it with the combinator many. Now if you want to add a rule like Exp ::= ( Exp ) you need to figure out whether to add it to Exp-norec or Exp-rec. Since the new rule is not left recursive, you can add it to Exp-norec: Exp-norec ::= Int | ( Exp-rec ) Exp-rec ::= Exp-norec | Exp-norec + Exp-rec If you implement this grammar with parser combinators, you should be able to parse (1+2)+3 just fine. Tillmann PS. Try adding multiplication to your grammar. You will need a similar trick to get the priorities right. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parser left recursion
Hi, Roman Cheplyaka wrote: Another workaround is to use memoization of some sort — see e.g. GLL (Generalized LL) parsing. Is there a GLL parser combinator library for Haskell? I know about the gll-combinators for Scala, but havn't seen anything for Haskell. Bonus points for providing the graph-structured stack (for maximal sharing in the computation) and the shared packed parse forest (for maximal sharing in the results) as reusable components. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda case (was Re: A big hurray for lambda-case (and all the other good stuff))
Hi, Brandon Allbery wrote: [...] syntax extension [...] I think someone's already working on this (SugarHaskell?). Yes, we are working on it. See our paper [1] and Sebastian's talk [2] at the Haskell Symposium. Our current prototype can be installed as an Eclipse plugin [3] or as a command-line tool [4]. [1] http://sugarj.org/sugarhaskell.pdf [2] http://www.youtube.com/watch?v=Kjm7bOLnuy0 [3] http://update.sugarj.org/ [4] http://hackage.haskell.org/package/sugarhaskell One use case we have in mind for SugarHaskell is prototyping of language extensions like the one discussed in this thread. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Categories (cont.)
Hi, Christopher Howard wrote: instance Category ... The Category class is rather restricted: Restriction 1: You cannot choose what the objects of the category are. Instead, the objects are always all Haskell types. You cannot choose anything at all about the objects. Restriction 2: You cannot freely choose what the morphisms of the category are. Instead, the morphisms are always Haskell values. (To some degree, you can choose *which* values you want to use). These restrictions disallow many categories. For example, the category where the objects are natural numbers and there is a morphism from m to n if m is greater than or equal to n cannot be expressed directly: Natural numbers are not Haskell types; and is bigger than or equal to is not a Haskell value. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Design of a DSL in Haskell
Hi Joerg,
Joerg Fritsch wrote:
I am interested in the definition of deep vs shallow embedded
I would say:
In shallow embedding, a DSL is implemented as a library. Every
keyword of the DSL is a function of the library. The
implementation of the function directly computes the result of
executing that keyword.
For example, here's a shallowly embedded DSL for processing
streams of integers:
{-# LANGUAGE TemplateHaskell #-}
module Stream where
import Prelude (Integer, (+), (*), (.))
import Language.Haskell.TH
data Stream = Stream Integer Stream
deriving Show
cycle x = Stream x (cycle x)
map f (Stream x xs) = Stream (f x) (map f xs)
There is one domain-specific type, Stream, and one
domain-specific operation, map. The body of map directly contains
the implementation of mapping over a stream. Correspondingly, DSL
programs are immediately evaluated to their values:
shallow :: Stream
shallow = map (+ 1) (map (* 2) (cycle 1))
In deep embedding, a DSL is implemented as a library. Every
keyword of the DSL is a function of the library. The implemention
of the function creates a structural representation of the DSL
program.
For example, here's a deeply embedded version of the above DSL:
data Program = Cycle Integer | Map (Integer - Integer) Program
Here, the domain-specific operations are data constructors. The example
program:
deep :: Program
deep = Map (+ 1) (Map (* 2) (Cycle 1))
We need a separate interpreter for actually executing the
program. The implementation of the interpreter can reuse cycle
and map from the shallow embedding:
eval :: Program - Stream
eval (Cycle x) = cycle x
eval (Map f p) = map f (eval p)
value :: Stream
value = eval deep
The benefit of deep embedding is that we can inspect the program,
for example, to optimize it:
optimize :: Program - Program
optimize (Cycle x) = Cycle x
optimize (Map f (Cycle x)) = Cycle (f x)
optimize (Map f (Map g s)) = optimize (Map (f . g) s)
value' :: Stream
value' = eval (optimize deep)
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Design of a DSL in Haskell
Hi, Joerg Fritsch wrote: is a shallow embedded DSL == an internal DSL and a deeply embedded DSL == an external DSL or the other way around? I mean internal == embedded, independently of deep vs. shallow, following Martin Fowler [1]. Tillmann [1] http://martinfowler.com/bliki/DomainSpecificLanguage.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Design of a DSL in Haskell
Hi, Joerg Fritsch wrote: I am working on a DSL that eventuyally would allow me to say: import language.cwmwl main = runCWMWL $ do eval (isFib::, 1000, ?BOOL) I have just started to work on the interpreter-function runCWMWL and I wonder whether it is possible to escape to real Haskell somehow (and how?) either inside ot outside the do-block. You can already use Haskell in your DSL. A simple example: main = runCWMWL $ do eval (isFib::, 500 + 500, ?BOOL) The (+) operator is taken from Haskell, and it is available in your DSL program. This use of Haskell is completely for free: You don't have to do anything special with your DSL implementation to support it. I consider this the main benefit of internal vs. external DSLs. A more complex example: main = runCWMWL $ do foo - eval (isFib::, 1000, ?BOOL) if foo then return 27 else return 42 Here, you are using the Haskell if-then-else expression to decide which DSL program to run. Note that this example also uses (=) and return, so it only works because your DSL is monadic. Beyond writing the Monad instance, you don't have to do anything special to support this. In particular, you might not need an additional embed function if you've already implemented return from the Monad type class. I consider this the main benefit of the Monad type class. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monads
Vasili I. Galchin wrote: I would an examples of monads that are pure, i.e. no side-effects. One view of programming in monadic style is: You call return and = all the time. (Either you call it directly, or do notation calls it for you). So if you want to understand whether a monad has side-effects, you should look at the implementation of return and =. If the implementation of return and = is written in pure Haskell (without unsafePerformIO or calling C code etc.), the monad is pure. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [ANNOUNCE] Fmark markup language
Hi, José Lopes wrote in an earlier email: I want to find a natural way of not burdening the user with the task of having to learn some special syntax in order to write a document. And then: [...] we can leave for quoting and use the ' for something else. That sounds like 'some special syntax' to me. Or should it be some special syntax? I can't remember which was for quoting and which was for something else. Maybe I need to look that up in the Fmark documentation, again. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Tutorial: Haskell for the Evil Genius
Hi, Kristopher Micinski wrote: Everyone in the Haskell cafe probably has a secret dream to give the best five minute monad talk. (1) Most programming languages support side effects. There are different kinds of side effects such as accessing mutable variables, reading files, running in parallel, raising exceptions, nondeterministically returning more than one answer, and many more. Most languages have some of these effects built into their semantics, and do not support the others at all. (2) Haskell is pure, so it doesn't support any side effects. Instead, when Haskell programmers want to perform a side effect, they explicitly construct a description of the side effecting computation as a value. For every group of related side effects, there is a Haskell type that describes computations that can have that group of side effects. (3) Some of these types are built in, such as IO for accessing the world outside the processor and ST for accessing local mutable variables. Other such types are defined in Haskell libraries, such as for computations that can fail and for computations that can return multiple answers. Application programmers often define their own types for the side effects they need to describe, tailoring the language to their needs. (4) All computation types have a common interface for operations that are independent of the exact side effects performed. Some functions work with arbitrary computations, just using this interface. For example, we can compose a computation with itself in order to run it twice. Such generic operations are highly reusable. (5) The common interface for constructing computations is called Monad. It is inspired by the mathematical theory that some computer scientists use when they describe what exactly the semantics of a programming language with side effects is. So most other languages support some monad natively without the programmer ever noticing, whereas Haskell programmers can choose (and even implement) exactly the monads they want. This makes Haskell a very good language for side effecting computation. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] map over Bijections
Hi,
Sergey Mironov wrote:
I need map equivalent for Bijection type which is defined in fclabels:
data Bijection (~) a b = Bij { fw :: a ~ b, bw :: b ~ a }
instance Category (~) = Category (Bijection (~)) where ...
I can define this function as follows:
mapBij :: Bijection (-) a c - Bijection (-) [a] [b] - Bijection (-) [a] [c]
mapBij b1 b = (map (fw b1)) `Bij` (map (bw b1))
Two observations.
First observation: The second argument seems unnecessary, so we have the
following instead:
mapBij :: Bijection (-) a c - Bijection (-) [a] [c]
mapBij b = (map (fw b)) `Bij` (map (bw b))
Second observation: I guess this works for arbitrary functors, not just
lists, so we get the following:
fmapBij :: Functor f = Bijection (-) a c - Bijection (-) (f a) (f c)
fmapBij b = (fmap (fw b)) `Bij` (fmap (bw b))
Lets check that fmapBij returns a bijection:
fw (fmapBij b) . bw (fmapBij b)
{- unfolding -}
= fmap (fw b) . fmap (bw b)
{- functor -}
= fmap (fw b . bw b)
{- bijection -}
= fmap id
{- functor -}
= id
Looks good.
I guess we can generalize this to get: If f is a functor on a category
c, it is also a functor on the category (Bijection c). But I am not sure
how to express this with Haskell typeclasses. Maybe along the lines of:
import Control.Categorical.Functor -- package categories
instance Endofunctor f cat = Endofunctor f (Bijection cat) where
fmap b = (fmap (fw b)) `Bij` (fmap (bw b))
So Bijection is a functor in the category of categories?
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fwd: 'let' keyword optional in do notation?
Hi, Martijn Schrage wrote: Would expanding each let-less binding to a separate let feel more sound to you? That was actually my first idea, but then two declarations at the same level will not be in the same binding group, so do x = y y = 1 would not compile. This would create a difference with all the other places where bindings may appear. But it would be in line with - bindings in the do notation, so maybe it wouldn't feel so wrong. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 3 level hierarchy of Haskell objects
Hi, Patrick Browne wrote: Haskell type classes seem to be signature only (no equations, ignoring default methods) so in general they provide an empty theory with no logical consequences. Note that many type classes in Haskell have equations annotated as comments. For example, the monad laws are mentioned in the documentation of the Monad type class: http://hackage.haskell.org/packages/archive/base/latest/doc/html/Prelude.html#t:Monad In this context, see also the current thread about what equations we can expect to hold for Eq instances: http://thread.gmane.org/gmane.comp.lang.haskell.cafe/99517 Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monads with The contexts?
Hi, Takayuki Muranushi wrote: sunPerMars :: [Double] sunPerMars = (/) $ sunMass * marsMass Sadly, this gives too many answers, and some of them are wrong because they assume different Earth mass in calculating Sun and Mars masses, which led to inconsistent calculation. This might be related to the problem adressed by Sebastian Fischer, Oleg Kiselyov and Chung-chieh Shan in their ICFP 2009 paper on purely functional lazy non-deterministic programming. http://www.cs.rutgers.edu/~ccshan/rational/lazy-nondet.pdf An implementation seems to be available on hackage. http://hackage.haskell.org/package/explicit-sharing Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Martin Odersky on What's wrong with Monads
Hi Rico,
Rico Moorman wrote:
data Tree = Leaf Integer | Branch (Tree Integer) (Tree Integer)
amount:: Tree - Integer
amount (Leaf x) = x
amount (Branch t1 t2) = amountt1 + amountt2
[...] additional requirement: If the command-line flag --multiply is set,
the function amount computes the product instead of the sum.
How would you implement this requirement in Haskell without changing the
line amount (Leaf x) = x?
The (for me at least) most obvious way to do this would be, to make the
operation to be applied to determine the amount (+ or *) an explicit
parameter in the function's definition.
data Tree a = Leaf a
| Branch (Tree a) (Tree a)
amount :: (a - a - a) - Tree a - a
amount fun (Leaf x) = x
amount fun (Branch t1 t2) = amount fun t1 `fun` amount fun t2
I agree: This is the most obvious way, and also a very good way. I would
probably do it like this.
Which drawbacks do you see besides increased verbosity?
Well, you did change the equation amount (Leaf x) = x to amount fun
(Leaf x) = x. In a larger example, this means that you need to change
many lines of many functions, just to get the the value of fun from the
point where it is known to the point where you need it.
[...] I am wondering which ways of doing this in Haskell you mean.
I thought of the following three options, but see also Nathan Howells
email for another alternative (that is related to my option (1) below):
(1) Implicit parameters:
{-# LANGUAGE ImplicitParams #-}
data Tree = Leaf Integer | Branch Tree Tree
amount :: (?fun :: Integer - Integer - Integer) = Tree - Integer
amount (Leaf x) = x
amount (Branch t1 t2) = ?fun (amount t1) (amount t2)
(2) Lexical Scoping:
data Tree = Leaf Integer | Branch Tree Tree
amount :: (Integer - Integer - Integer) - Tree - Integer
amount fun = amount where {
amount (Leaf x) = x
; amount (Branch t1 t2) = fun (amount t1) (amount t2) }
(3) UnsafePerformIO:
import System.IO.Unsafe (unsafePerformIO)
data Tree = Leaf Integer | Branch Tree Tree
amount :: Tree - Integer
amount (Leaf x) = x
amount (Branch t1 t2) = fun (amount t1) (amount t2)
where fun = unsafePerformIO ...
I'm not happy with any of these options. Personally, I would probably go
ahead and transform the whole program just to get the value of fun to
where it is needed. Nevertheless, having actually done this before, I
understand why Martin Odersky doesn't like doing it :)
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Martin Odersky on What's wrong with Monads
Hi, MightyByte wrote: Of course every line of your program that uses a Foo will change if you switch to IO Foo instead. But we often have to also change lines that don't use Foo at all. For example, here is the type of binary trees of integers: data Tree = Leaf Integer | Branch (Tree Integer) (Tree Integer) A function to add up all integers in a tree: amount:: Tree - Integer amount (Leaf x) = x amount (Branch t1 t2) = amountt1 + amountt2 All fine so far. Now, consider the following additional requirement: If the command-line flag --multiply is set, the function amount computes the product instead of the sum. In a language with implicit side effects, it is easy to implement this. We just change the third line of the amount function to check whether to call (+) or (*). In particular, we would not touch the other two lines. How would you implement this requirement in Haskell without changing the line amount (Leaf x) = x? (I actually see three ways of doing this in Haskell, but all have serious drawbacks and do not fully solve the problem). Here it seems not so bad just to change all three lines of the amount function, even if they are not strictly related to the semantic change we want to make. But in a real program, this situation can translate to changing thousands of lines of code in many functions just to implement a minor change to a single requirement. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: set-monad
Hi George, thanks for your detailed reply. George Giorgidze wrote: The key to the approach used in set-monad is to make progress with the evaluation of the unconstrained constructors (i.e., Return, Bind, Zero and Plus) without using constrained set-specific operations. It turns out that for several cases one can progress with the evaluation without duplicating f (evaluation relies on monoid laws, Plus is associative and Zero is left and right identity of Plus). I have pushed those optimisations to the repo. These optimisations also cover your example. Cool. In your email, you have also asked: I suspect that I can achieve similar results by using the list monad and converting to a set in the very end. In what situations can I benefit from set-monad? Sometimes set is a more appropriate data structure than list. [...] Of course. But I was wondering whether something like set-monad could be implemented with newtype Set a = Set [a] instead of data Set a = Prim ... | Return ... | Bind ... | ... Both approaches can offer the same interface, but now I think I see two reasons why the latter is more efficient than the former: (1) It allows to use set-operations when an Ord is known, for example, when the user calls union, and (2) It allows optimizations like you describe above. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Layout Rule
Hi Michael, Michael D. Adams wrote: I am looking for background material on how GHC and other Haskell compilers implement the layout rule. In the context of our work on syntactic extensibility, we have implemented a declarative and extensible mechanism to specify and implement layout rules. A paper about the approach is currently under review, and a draft is available [1]. The implementation and evaluation data is available [2]. [1] http://sugarj.org/layout-parsing.pdf [2] http://github.com/seba--/layout-parsing We used our parser in the implementation of SugarHaskell, a syntactically extensible variant of Haskell. A paper about SugarHaskell is currently under review, and again, a draft is available [3]. The implementation can be installed as an Eclipse plugin from the SugarJ website [4]. A command-line version is forthcoming. [3] http://sugarj.org/sugarhaskell.pdf [4] http://sugarj.org/ Best Regards, Tillmann (on behalf of the SugarJ team) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: set-monad
Hi, David Menendez wrote: As you noticed, you can get somewhat better performance by using the combinators that convert to S.Set internally, because they eliminate redundant computations later on. Somewhat better? My example was three times faster, and I guess that the fast variant is O(n) and the slow variant is O(n²). So I expect that for some applications, the Set interface is more than fast enough and the MonadPlus-interface is much too slow. (Why is unioned faster then numbers? Is union doing some rebalancing? Can I trigger that effect directly?) It's because mplus a b= f turns into mplus (a= f) (b= f), whereas unioned takes the union before calling f. Here, you compare mplused to unioned, but in the parentheses, I asked about numbers and unioned (from my last email). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: set-monad
Hi George,
George Giorgidze wrote:
I would like to announce the first release of the set-monad library.
On Hackage: http://hackage.haskell.org/package/set-monad
Very cool. Seems to work fine. But I am wondering about the impact of
using your package on asymptotic complexity (and thereby, on performance).
From your implementation:
data Set a where
Prim :: (Ord a) = S.Set a - Set a
[...]
Zero :: Set a
Plus :: Set a - Set a - Set a
I notice that this part of your datatype looks like a binary tree of
sets. Lets see how your run function treats it:
run :: (Ord a) = Set a - S.Set a
run (Prim s) = s
[...]
run (Zero)= S.empty
run (Plus ma mb) = S.union (run ma) (run mb)
As expected, the Prim-Zero-Plus structure is treated as a binary tree of
sets, and run collects all the sets together. That is probably fine,
because it should have the same complexity as combining these sets in
the first place.
run (Bind (Prim s) f) = S.foldl' S.union S.empty (S.map (run . f) s)
[...]
run (Bind Zero _) = S.empty
run (Bind (Plus ma mb) f) = run (Plus (Bind ma f) (Bind mb f))
[...]
But when I use the binary tree of sets on the left-hand side of a bind,
your run function has to naively traverse the whole tree. So if the same
elements are included in many sets in the tree of sets, these elements
will be processed more than once, so the overall complexity is worse
than necessary.
Here's a ghci session that seems to confirm my suspicion. I first define
a function using set-monad's convenient monad instance for sets:
$ :m +Control.Monad Data.Set.Monad
$ let s1 `times` s2 = do {e1 - s1; e2 - s2; return (e1, e2)}
Now I produce some test data:
$ let numbers = fromList [1 .. 1000]
$ let unioned = numbers `union` numbers
$ let mplused = numbers `mplus` numbers
Note that these three sets are all equivalent.
$ (numbers == unioned, numbers == mplused, unioned == mplused)
(True, True, True)
However, they behave differently when passed to the times function
above. numbers and unioned are similarly fast:
$ :set +s
$ size $ numbers `times` numbers
100
(2.56 secs, 1315452984 bytes)
$ size $ unioned `times` unioned
(2.39 secs, 1314950600 bytes)
100
(Why is unioned faster then numbers? Is union doing some rebalancing?
Can I trigger that effect directly?)
But mplused is much slower:
$ size $ mplused `times` mplused
100
(10.83 secs, 5324731444 bytes)
I suspect that I can achieve similar results by using the list monad and
converting to a set in the very end. In what situations can I benefit
from set-monad?
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Typed TemplateHaskell?
Hi Ilya, Ilya Portnov wrote: As far as can I see, using features of last GHC one could write typed TH library relatively easily, and saving backwards compatibility. For example, now we have Q monad and Exp type in template-haskell package. Let's imagine some new package, say typed-template-haskell, with new TQ monad and new polymorphic type Exp :: * - *. Using last GHC's features, one will easily write something like expr :: Exp String, which will mean that expr represents a string expression. And we will need a new function, say runTQ :: TQ a - Q a (or some more complicated type), which will turn TypedTemplateHaskell's constructs into plain TH. That would be a good thing to have. But it might be quite hard to implement. For example, I guess you might want to have functions like this one: apply :: Exp (a - b) - Exp a - Exp b This function takes two typed expressions and produces an application. The types ensure that the generated application will typecheck. Cool. But can you do the same thing for lambdas? Lambdas create functions, so the type would be something like the following: lambda :: ... - Exp (a - b) But what would you put instead of the ...? I fear that overall, you would have to reimplement Haskell's type system in Haskell's type system. Which sounds like a cool thing to do, but maybe not so easily. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: unfoldable-0.4.0
Hi, Sjoerd Visscher wrote: Just as there's a Foldable class, there should also be an Unfoldable class. This package provides one: class Unfoldable t where unfold :: Unfolder f = f a - f (t a) Just to be sure: That's not a generalization of Data.List.unfoldr, or is it somehow? Different unfolders provide different ways of generating values, for example: - Random values - Enumeration of all values (depth-first or breadth-first) - Convert from a list - An implementation of QuickCheck's arbitrary should also be possible (still working on that) Can this be extended to provide a single API that allows testing à la SmallCheck, LazySmallCheck and/or QuickCheck without duplicating properties or instances? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I Need a Better Functional Language!
Paul R wrote: I am curious what are interesting use-cases for that? Symbolic analysis? self-compilers? Optimization. For example, imagine the following definition of function composition: map f . map g = map (f . g) f . g = \x - f (g x) In Haskell, we cannot write this, because we cannot pattern match on function calls. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Are there arithmetic composition of functions?
Hi, sdiy...@sjtu.edu.cn wrote: I feel it would be very natural to have in haskell something like g::Float-Float --define g here h::Float-Float --define h here f::Float-Float f = g+h --instead of f t = g t+h t --Of course, f = g+h is defined as f t = g t+h t One approach to achieve this is to define your own version of +, using the equation in the last comment of the above code snippet: (g .+. h) t = g t + h t Now you can write the following: f = g .+. h You could now implement .*., ./. and so on. (I use the dots in the operator names because the operator is applied pointwise). The implementations would look like this: (g .+. h) t = g t + h t (g .*. h) t = g t * h t (g ./. h) t = g t / h t This is a bit more low-tech than the proposals in the other answers, but might be good enough for some applications. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theoretical question: are side effects necessary?
Hi, Christopher Svanefalk wrote: Are there any problems which *cannot* be solved a side effect-free language (such as Haskell)? No. Haskell is expressive enough. One way to prove that is to implement an interpreter for a language with side effects in Haskell. Now if there's a program P to solve a problem in the language-with-side-effects, we can run that interpreter on P to solve the same problem in Haskell. The interpreter could use a Data.Map to associate variable names with values. That would probably not be the fastest or the most memory efficient implementation of the language-with-side-effects, but it would work. The same trick of implementing one language in the other can be done for almost every pair of reasonably expressive languages, so they are all equally expressive in a sense. It is even widely believed that no even more expressive language can exist. That means that if a problem can be solved by a computer at all, it can also be solved using any of these reasonably expressive languages. That is the Church-Turing-Hypothesis. (And the other way around: if the hypothesis is true, and a problem can not be solved in one of these languages, that problem cannot be solved with a computer at all. Unfortunately, many interesting problems are like that). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] puzzling polymorphism behavior (7.0.3 windows)
Hi, this is one of the reasons why unsafePerformIO is not type-safe. Lets see what's going on by figuring out the types of the various definitions. cell = unsafePerformIO $ newIORef [] newIORef returns a cell which can hold values of the same type as its arguments. The type of the empty list is [a], because an empty list could be a list of arbitrary elements. So the overall type of cell is: cell :: IORef [a] cell returns a cell which can hold lists of arbitrary elements. push i = modifyIORef cell (++ [i]) Lets say i is of some type b. Then cell needs to hold lists of the type b. So in this use of cell, the type variable is instantiated to b, and the overall type of push is: push :: b - IO () So push can accept arbitrary values, and appends them to the list hold by cell. (Note that ghc reports the type as (a - IO ()), but that really means the same thing as (b - IO ()). main = do push 3 Here, since you call push with 3, b is chosen to be Int. After this line, the cell holds the list [3]. push x Here, since you call push with x, b is chosen to be String. After this line, the cell holds the list [3, x], which is not well-typed. You tricked Haskell to produce an ill-typed list by using unsafePerformIO. readIORef cell = return Here, it is not clear how you want to instantiate the type variable a in the type of cell. So lets assume that we want to return a value of type c, and instantiate a with c. So even though at this point, the list contains an Int and a String, we can (try to) extract whatever type we want from the list. Therefore, the overall type of main is: main :: IO [c] *Main main [(),()] Now once more, it is not clear how you want to instantiate c, so, by default, () is chosen. That default is only active in ghci, by the way. main will extract the Int 3 and the String x from the list, but treat them as if they were of type (). Here you get lucky: Since there's only one value of type (), ghci can show () without looking at it too deeply, so even though this program is not type-safe in a sense, it works fine in practice. But try forcing ghci to consider a more interesting type instead of (): *Main main :: IO [Int] [3,738467421] The string x is reinterpreted as a number and shown as such. You can try other types instead of Int until your ghci crashes because you access some memory you shouldn't have looked at or try to execute some random part of your memory as code. So to summarize, your code exhibits the (well-known) fact that unsafePerformIO is not type-safe, because it can be used to implement a polymorphic reference, which is a Bad Thing. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: exists-0.1
Hi, Gábor Lehel wrote: data E = forall a. C a = E a I don't know if anyone's ever set out what the precise requirements are for a type class method to be useful with existentials. More than you seem to think. For example: data Number = forall a . Num a = Number a foo :: Number - Number foo (Number x) = Number (x * x + 3) So the binary operation (*) can be used. Note that from a type-checking perspective, the pattern match on (Number x) also extracts the type, which is then available when checking the right-hand side. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
Hi, Robert Clausecker wrote: Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different? I would try to improve the language's support for the embedding of domain-specific embedded languages (aka. combinator libraries). Such embedding requires the integration of a domain-specific language's syntax, static semantics and dynamic semantics. Some (more or less far fetched) ideas about these three areas follow. To support better syntax for embedded languages, provide more rebindable syntax à la do-notation. For example, (if c then t else e) currently desugars to (case c of False - e; True - t). But it could also desugar to (if' c t e) where if' is a method of a type class. For (c : Bool), the standard library would provide an instance of this type class, but for other condition types, third-party libraries could provide it. Alternatively, if-then-else could even desugar to whatever if' is in scope. A similar idea is currently applied to Scala in the scala-virtualized project. A large part of the language should be virtualized this way, including pattern matching, lambda expressions, maybe even type or class declarations. To support better static semantics for embedded languages, provide better type-level computation, including some form of closed-world reasoning (for example, backtracking or closed pattern matching) and a reification of names at the type level, so that type-level computations can reason about the binding structures of expressions-level code. Note that I am interested in the static structure of terms, not their dynamic behavior, so this is different from dependent types. With Haskell being a fine general-purpose programming language, and even having a good foreign language interface, there is already plenty of support for the specification of dynamic semantics. Nevertheless, for domain-specific embedded compilers, it would possibly be nice to access a Haskell compiler at runtime, to compile snippets of Haskell code and dynamically link them into the currently running program. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Putting constraints on internal type variables in GADTs
Hi, Anupam Jain wrote: -- My datatype data T o where Only ∷ o → T o TT ∷ T o1 → (o1 → o2) → T o2 -- Show instance for debugging instance Show o ⇒ Show (T o) where show (Only o) = Only ⊕ (show o) show (TT t1 f) = TT ( ⊕ (show t1) ⊕ ) As you noticed, the last line doesn't work because t1 is of some unknown type o1, and we know nothing about o1. In particular, we don't know how to show values of type t1, neither at compile time nor at runtime. I can't see a way around that. However, for debugging, you could do: show (TT t1 f) = TT ( ++ show (f t1) ++ ) This is not perfect, but at least it should work. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: remove Stability from haddock documentation on hackage
Hi, James Cook wrote: As far as Control.Applicative, I'm not sure to what package you're referring. That label doesn't apply to modules, it applies to packages, and Control.Applicative is a part of the base package (which is not labeled experimental). On http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Applicative.html, in the upper right corner, the module is marked as experimental. I think this is a Haddock feature, not a Hackage feature. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] representing spreadsheets
Hi, Eric Rasmussen wrote: The spreadsheet analogy isn't too literal as I'll be using this for data with a more regular structure. For instance, one grid might have 3 columns where every item in column one is a CellStr, every item in column two a CellStr, and every item in column 3 a CellDbl, but within a given grid there won't be surprise rows with extra columns or columns that contain some cell strings, some cell ints, etc. Sounds more like a database than like a spreadsheet. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] object oriented technique
Hi,
Steffen Schuldenzucker wrote:
data Shape = Shape {
draw :: String
copyTo :: Double - Double - Shape
}
Tad Doxsee wrote:
Suppose that the shape class has 100 methods and that 1000 fully
evaluated shapes are placed in a list.
The above solution would store the full method table with each object.
Instead, we could share the method tables between objects. An object
would then uniformly contain two pointers: One pointer to the method
table, and one poiner to the internal state.
{-# LANGUAGE ExistentialQuantification, Rank2Types #-}
data Object methods = forall state . Object {
methods :: methods state,
state :: state
}
Calling a method requires dereferencing both pointers.
call :: (forall state . methods state - state - a) -
(Object methods - a)
call method (Object methods state) = method methods state
Using this machinery, we can encode the interface for shapes.
data ShapeClass state = ShapeClass {
draw :: state - String,
copyTo :: state - Double - Double - Shape
}
type Shape = Object ShapeClass
An implementation of the interface consists of three parts: A datatype
or the internal state, a method table, and a constructor.
data RectangleState = RectangleState {rx, ry, rw, rh :: Double}
rectangleClass :: ShapeClass RectangleState
rectangleClass = ShapeClass {
draw = \r -
Rect ( ++ show (rx r) ++ , ++ show (ry r) ++ ) --
++ show (rw r) ++ x ++ show (rh r),
copyTo = \r x y - rectangle x y (rw r) (rh r)
}
rectangle :: Double - Double - Double - Double - Shape
rectangle x y w h
= Object rectangleClass (RectangleState x y w h)
The analogous code for circles.
data CircleState = CircleState {cx, cy, cr :: Double}
circleClass :: ShapeClass CircleState
circleClass = ShapeClass {
draw = \c -
Circ ( ++ show (cx c) ++ , ++ show (cy c)++ ) --
++ show (cr c),
copyTo = \c x y - circle x y (cr c)
}
circle :: Double - Double - Double - Shape
circle x y r
= Object circleClass (CircleState x y r)
Rectangles and circles can be stored together in usual Haskell lists,
because they are not statically distinguished at all.
-- test
r1 = rectangle 0 0 3 2
r2 = rectangle 1 1 4 5
c1 = circle 0 0 5
c2 = circle 2 0 7
shapes = [r1, r2, c1, c2]
main = mapM_ (putStrLn . call draw) shapes
While this does not nearly implement all of OO (no inheritance, no late
binding, ...), it might meet your requirements.
Tillmann
PS. You could probably use a type class instead of the algebraic data
type ShapeClass, but I don't see a benefit. Indeed, I like how the code
above is very explicit about what is stored where. For example, in the
code of the rectangle function, it is clearly visible that all shapes
created with that function will share a method table.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy evaluation and tail-recursion
Hi, Daniel Fischer wrote: Let's look at the following code: countdown n = if n == 0 then 0 else foo (n - 1) s/foo/countdown/ presumably if' c t e = if c then t else e countdown' n = if' (n == 0) 0 (foo (n - 1)) s/foo/countdown'/ Yes to both substitutions. Looks like I need an email client with ghc integration. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type trickery
Hi Andrew, Andrew Coppin wrote: You could define a function: withContainer ∷ (∀ s. Container s → α) → α which creates a container, parameterizes it with an 's' that is only scoped over the continuation and applies the continuation to the created container. Hmm, yes. That will work, but I wonder if there's some way of doing this that doesn't limit the scope of the container to one single span of code... You can write helper functions which take containers as argument by parameterizing these helper functions over s: takesTwoContainers :: Container s1 - Container s2 - ... takesTwoContainers c1 c2 = ... -- c1 and c2 can be used here This function could be called like this: withContainer (\c1 - withContainer (\c2 - takesTwoContainers c1 c2)) -- c1 and c2 can be used here In this example, the scope of the containers is not limited to a single span of code. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy evaluation and tail-recursion
Hi, Yves Parès wrote: A question recently popped into my mind: does lazy evaluation reduce the need to proper tail-recursion? I mean, for instance : fmap f [] = [] fmap f (x:xs) = f x : fmap f xs Here fmap is not tail-recursive, but thanks to the fact that operator (:) is lazy, I think that it may still run in constant space/time, am I right? In a sense, that definition of fmap is tail-recursive. To see that, consider how a non-strict list could be encoded in a strict language: data EvaluatedList a = Cons a (List a) | Empty type List a = () - EvaluatedList a map :: (a - b) - (List a - List b) map f xs = \_ - case xs () of Cons x xs - Cons (f x) (\_ - map f xs ()) Empty - Empty Here, the call to map is more visibly in tail position. So I would say that in Haskell, tail-call optimization is just as important as, for example, in Scheme. But tail positions are not defined syntactically, but semantically, depending on the strictness properties of the program. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy evaluation and tail-recursion
Hi, Daniel Fischer wrote: data EvaluatedList a = Cons a (List a) | Empty type List a = () - EvaluatedList a map :: (a - b) - (List a - List b) map f xs = \_ - case xs () of Cons x xs - Cons (f x) (\_ - map f xs ()) Empty - Empty Here, the call to map is more visibly in tail position. According to the definition of tail recursion that I know, that's not tail recursive. My point is that the call to map is in tail position, because it is the last thing the function (\_ - map f xs ()) does. So it is not a tail-recursive call, but it is a tail call. Of course, (\_ - map f xs ()) does not occur literally in the Haskell implementation of map, but the runtime behavior of the Haskell implementation of map is similar to the runtime behavior of the code above in a strict language. Let's look at the following code: countdown n = if n == 0 then 0 else foo (n - 1) if' c t e = if c then t else e countdown' n = if' (n == 0) 0 (foo (n - 1)) countdown is clearly tail-recursive. Because of Haskell's non-strict semantics, countdown and countdown' have the same runtime behavior. I therefore submit that countdown' is tail-recursive, too. So I think that in a non-strict language like Haskell, we need to define tail position semantically, not syntactically. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Question on a common pattern
Hi, Donn Cave wrote: someIO= f where f Opt1 = ... I like this ... or, I would like it, if I could make it work! I get The last statement in a 'do' construct must be an expression, Where-clauses can only be used on equations, not on expressions or statements, so you would need to float the where clause outwards: foo = do someIO = f where f = ... Or you can use let-in-expressions or let-statements to bind local values (or functions) in do-notation: do let f = ... result - someIO = f or do result - let f = ... in someIO = Op1 = .. HTH, Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Examples for the problem
Hi, Robert Clausecker wrote: Each instruction has up to three operands, looking like this: @+4 (Jump for bytes forward) foo (the string foo '0'(1+2) etc. A string literal may contain anything but a newline, (there are no escape codes or similar). But when I add a check for a newline, the parser just fails and the next one is tried. This is undesired, as I want to return an error like unexpected newline instead. How is this handled in other parsers? I would expect that the other parsers are tried, but fail, because they do not accept an initial quotation mark. You get two errors messages then: 1. Unexpected newline after quotation mark 2. Unexpected quotation mark These two error messages reflect the two ways to solve the problem: Either delete the first quotation mark, or add a second one. Tillmann PS. Please use Reply to answer posts, so that they can be put into the same thread. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rebindable 'let' for observable sharing?
Hi, Bas van Dijk wrote: For the record: are you talking about rewriting: let f = e in b into something like: (\f - e) `letin` (\f - b) where `letin` can be overloaded (rebinded is probably the better term) and has the default implementation: letin :: (a - a) - (a - b) - b fe `letin` fb = fb (fix fe) I don't see how this captures the static semantics of let. In the original code, f can be polymorphic, but in the desugared version, f is monomorphic. Maybe the following works with an appropriate set of extensions enabled: First, infer the type of f in (let f = e in b) and call it T. Then, rewrite (let f = e in b) to ((\f :: T - e) `letin` (\f - b)). But Henning's original goal to open a way to implement observable sharing as needed in EDSLs by a custom 'fix' might be easier to achieve by desugaring let expressions into let expressions with some extra function applications: let f = e in b would become something like let f = hook1 e in hook2 f b Now, hook1 would default to id, and hook2 would default to (const id). I think this would capture the static and dynamic semantics of let expressions, and it might be enough to implement observable sharing. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Performance difference between ghc and ghci
Hi, C K Kashyap wrote: I missed out the optimization bit yes, that would make a difference. However beyond that is it not just about graph reduction which should be the same? Even if the number of reduction steps is the same, the bytecode interpreter is still slower than compiled code, because it takes more processor cycles per reduction step. This interpretative overhead could be avoided, for example, using just-in-time compilation à la Smalltalk or Java. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
Pedro Vasconcelos wrote: This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking. For example, the type signature for a variable swapping procedure in C: void swap(int *a, int *b) This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair: swap :: (Int,Int) - (Int,Int) This benefit of explicit input and output values can interact nicely with parametric polymorphism: swap :: (a, b) - (b, a) This more general type signature makes sure we are not just returning the input values unswapped. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] combined parsing pretty-printing
Hi Ozgur, Ozgur Akgun wrote: I can write (separately) a parser and a pretty-printer [...] Is there any work to combine the two? Brent Yorgey wrote: Maybe take a look at Invertible Syntax Descriptions: Unifying Parsing and Pretty Printing by Tillmann Rendel and Klaus Ostermann from last year's Haskell Symposium: http://www.informatik.uni-marburg.de/~rendel/unparse/ It's a beautiful paper, and perhaps the code will work for you (although it's too bad it's not on Hackage). Indeed, I started this project for exactly the reason Ozgur describes: I needed to duplicate a lot of information between parsers and pretty printers and was annoyed about it. With invertible syntax descriptions, I now write a single program, which looks like a combinator parser (think Parsec), but can work as a pretty printer, too. I just uploaded the code from the paper (and some additional combinators) to Hackage: http://hackage.haskell.org/package/partial-isomorphisms http://hackage.haskell.org/package/invertible-syntax I use this code for the implementation of some very small languages (think lambda calculus). This works fine. I haven't really tried it for larger languages, but we have two students here in Marburg implementing a parser for Java using the library, so we are going to have experience with larger languages in a few weeks (months?). If you give it a try, I would be happy to receive success stories, bug reports, patches, feature requests etc. I want to keep working on this, and I am open for suggestions. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reader monad
Hi, Michael Rice wrote: I think of (r - m a) as a type signature and Int or Bool by themselves as types. So, all type signatures are themselves types? Yes. In Haskell, functions are first class, so function types like (r - m a) are themselves types. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Template Haskell a Permanent solution?
Hi,
Jonathan Geddes wrote:
For TH use #1, compile-time parsing of arbitrary strings, I think it
would be nice for quasiquote semantics to be modified so that code
like
json :: String - JsonObject
json = ...
data = [ json |
{ name : Jonathan
, favorite language: Haskell
}
|]
causes the function json to be called at compile time with a string
argument of{\name\ : \Jonathan\\n , \favorite language\:
\Haskell\\n }. The whole expression being then replaced with the
result of the function application. What I like about this is that
defining quasiquoters is trivial. They're just functions of the form
String - a. Many such quasiquoters already exist and would be ready
for use! I imagine certain rules would apply, ie a quasiquoter must be
defined prior to use and in a separate module, etc.
First note that this is just quotation, not yet quasiquotation. For
quasiquotation, you would also need to support antiquotation (i.e., the
use of Haskell identifiers or even expressions in the middle of quoted
syntax). And to reach something similar to the current support for
quasiquotation, you would need to support patterns etc., too.
Secondly, I was going to propose to use generic programming to convert
from a parser like (String - JsonObject) to a quasiquoter for Json. But
after half a day of experiments, I figured out that this idea is already
developed in
Geoffrey B. Mainland.
Why It's Nice to be Quoted: Quasiquoting for Haskell.
Haskell Workshop 2007
Available at:
http://www.eecs.harvard.edu/~mainland/publications/mainland07quasiquoting.pdf
In that paper, Geoffrey Mainland explains how a parser can be
generically upgraded to a quoter, reaching an intermediate conclusion on
page 6:
By using generic programming, we can take a parser and create
expression and pattern quasiquoters for the language it parses with
only four lines of code, including type signatures! This holds not
just for our simple object language, but for any object language.
He goes on to explain how to add support for antiquotation [...] with
only slightly more than four lines of code.
The functions dataToExpQ and dataToPatQ from that paper are available in
the TH library in Language.Haskell.TH.Quote. A simple helper function
quasiQuoter :: Data a = (String - Either String a) - QuasiQuoter
quasiQuoter parser = QuasiQuoter
{ quoteExp = either fail (dataToExpQ (const Nothing)) . parse
, quotePat = either fail (dataToPatQ (const Nothing)) . parse
}
should allow you to write your JSON example as follows:
parse :: String - Either String JsonObject
parse = ...
json = quasiQuoter parse
This seems simple enough to me, so it looks as if your use case is
already supported as a library on top of the more general API.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Functor = Applicative = Monad
Hi John,
John Smith wrote:
Perhaps pattern match failures in a MonadPlus should bind to mzero - I
believe that this is what your example and similar wish to achieve.
You updated the proposal to say:
a failed pattern match should error in the same way as is does for pure code,
while in
MonadPlus, the current behaviour could be maintained with mzero
Can you be more specific as to how that would interact with polymorphism
and type inference? What does it mean to be in MonadPlus? How does the
compiler know?
For example, what would be the static types and dynamic semantics of the
following expressions:
1. \a - do {Just x - return (Just a); return x}
2. do {Just x - return Nothing; return x}
3. \a - do {Just x - a; return x}
4. \a b - do {(x, _) - return (a, b); return x}
5. \a - do {(x, _) - return a; return x}
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Functor = Applicative = Monad
John Smith proposed: a failed pattern match should error in the same way as is does for pure code, while in MonadPlus, the current behaviour could be maintained with mzero Lennart Augustsson wrote: Any refutable pattern match in do would force MonadFail (or MonadPlus if you prefer). I guess that would work out, but I think John proposed something else. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Functor = Applicative = Monad
Hi, John Smith wrote: I would like to formally propose that Monad become a subclass of Applicative A lot of code would break because of this change, but all problems should be reported at compile time, and are easy to fix. In most of the cases, either adding obvious Functor and Applicative instances to a library; or deleting such instances from a client, I would expect. This kind of clean-up would actually increase the quality of the library, however, and might therefore be acceptable. The change is described on the wiki at http://haskell.org/haskellwiki/Functor-Applicative-Monad_Proposal There you write, among other things: fail should be removed from Monad; a failed pattern match could error in the same way as is does for pure code. How is this part of the proposal related to Functor and Applicative? Since code depending on the current behavior can not be detected at compile time, this is a more serious change in a way: code keeps compiling but changes its meaning. Can you estimate how much code would break because of this change? Would it be possible to keep user-defined failure handling in do notation without keeping fail in Monad? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Re: Reply-To: Header in Mailinglists
Hi, Nick Bowler wrote: There is another header, Mail-Followup-To, which tells MUAs to also drop the To and CC lists. Interesting. So is it a good idea to use Mail-Followup-To to move a discussion from one list to another? To: hask...@haskell.org CC: haskell-cafe@haskell.org Mail-Followup-To: haskell-cafe@haskell.org Subject: Foo on the iPhone (was: [Haskell] [ANN] Foo released!) Or should I rather swap To and CC? Or leave out hask...@... completely? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
Hi Andrew, Andrew Coppin wrote: Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. What do you mean by hold the same thing at all times? Consider the following program: id :: forall a . a - a id x = x call1 :: Bool call1 = id True call2 :: Int call2 = id 42 This program contains a type variable a, and a value variable x. Now, these variables do *not* mean the same thing at all times. In the first call of id, a is Bool and x is True; but in the second call of id, a is Int and x is 42. If these variables would mean the same thing at all times, I would expect them to be called constants, wouldn't you? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
Ketil Malde wrote: data Sum a b = A a | B b -- values = values in a + values in b data Prod a b = P a b-- values = values in a * values in b I guess this makes [X] an exponential type, although I don't remember seeing that term :-) I would expect the exponential type to be (a - b): type Exp b a = a - b -- values = values in b ^ values in a Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reply-To: Header in Mailinglists
Hi Bastian, Bastian Erdnüß wrote: It would make my life a little bit more easy if the mailing lists on haskell.org would add a Reply-To: header automatically to each message containing the address of the mailing list, the message was sent to. Usually that's the place where others would want to sent the answers to, I would suppose. The mailing lists on haskell.org set the List-Post: header to the adress of the list, and many mail clients use this information to allow reply to list somehow. If your client doesn't, you can manually work around the problem by reply to all and possibly deleting the email adress of the original sender. I use Mozilla Thunderbird 3.1.6, and I have configured it to show a button reply to list between reply to all and forward. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] intent-typing
Hi, Marcus Sundman wrote: Hi, how would one go about implementing (or using if it's supported out-of-the-box) intent-typing* for haskell? A basic technique is to use newtype declarations to declare separate types for separate intents. module StringSafety ( SafeString () , UnsafeString () , quote , considerUnsafe ) where newtype SafeString = SafeString String newtype UnsafeString = UnsafeString String considerUnsafe :: String - UnsafeString considerUnsafe s = UnsafeString s quote :: UnsafeString - SafeString quote (UnsafeString s) = SafeString s' where s' = ... s ... This module does not export the SafeString and UnsafeString constructors, so we can be sure that no other code in the program can invent SafeStrings which are not really safe. Every string can be safely treated as unsafe, however, so we export a function considerUnsafe which does so. Now, if we type our interface to the outside world as getInput :: ... - UnsafeString sendOutput:: SafeString - ... we can be sure that a return value from getInput needs to pass through quote on its way to sendOutput, because quote is the only way to produce a SafeString. This guarantuees safety. It has, however, a practical problem: We can't use the usual String functions on UnsafeString or SafeString values. For instance, we can't concatenate two UnsafeStrings using (++). A naive solution would be to provide separate (++) functions for unsafe and safe strings: append_safe :: SafeString - SafeString - SafeString append_safe (SafeString x) (SafeString y) = SafeString (x ++ y) append_unsafe :: SafeString - SafeString - SafeString append_unsafe (UnsafeString x) (UnsafeString y) = UnsafeString (x ++ y) Note that at least append_safe needs to be implemented in and exported from the StringSafety module. That is a good thing, because this function needs to be carefully checked for safety. The programmer needs to prove (or unit-test, or at least think about) the following theorem: If a and b are safe strings, so is a ++ b. After this fact has been established, other modules are free to use append_safe however they like without possibly compromising safety. Now, the above approach should work, but is still rather impractical: We need to copy the definitions of all String functions for unsafe and safe strings. However, since the bodies of all these copies are actually identical, so we can use parametric polymorphism to abstract over the difference between UnsafeString and SafeString. One way to achieve this is to use phantom types. With phantom types, we declare only a single newtype for both safe and unsafe strings, but we annotate that type with an additional flag to distinguish safe from unsafe uses. module StringSafety ( AnnotatedString () , Safe () , Unsafe () , quote , considerUnsafe , append ) where data Safe = Safe data Unsafe = Unsafe newtype AnnotatedString safety = AnnotatedString String considerUnsafe :: String - AnnotatedString Unsafe considerUnsafe s = AnnotatedString s quote :: AnnotatedString Unsafe - AnnotatedString Safe quote (AnnotatedString s) = AnnotatedString s' where s' = ... s ... append :: AnnotatedString a - AnnotatedString a - AnnotatedString a append (AnnotatedString x) (AnnotatedString y) = AnnotatedString (x ++ y) Note that AnnotatedString does not really use its type parameter safety: That's why it is called a phantom type. The data constructor AnnotatedString can be freely used to convert between safe and unsafe strings, so we better not export it from the module. Inside the module, uses of the data constructor gives rise to proof obligations as above. So the programmer needs to reason that the following is true to justify the implementation and export of append: If x and y have the same safety level, then (x ++ y) has again that same safety level. So now, we still have to write a wrapper around each string operation, but at least we need to write only one such wrapper for all intents, not a separate wrapper for each intent. There is an inconvenience left: We can't concatenate safe and unsafe strings, because both arguments to append need to have exactly the same type. To fix this, we first have to figure out what the result of sucha concatenation would be: It would be an unsafe string, because at least one of the inputs is unsafe. We need to teach this kind of reasoning to the compiler, for instance, using type families: type family Join a b type instance Join Safe Safe = Safe type instance Join Safe Unsafe = Unsafe type instance Join Unsafe Safe = Unsafe type instance Join Unsafe Unsafe = Unsafe The idea is that (Join a b) is the safety level of the result of an operation which
Re: [Haskell-cafe] Serialization of (a - b) and IO a
Andrew Coppin wrote: [...] if you could send a block of code from one PC to another to execute it remotely. Eden can do this. http://www.mathematik.uni-marburg.de/~eden/ Eden is a distributed Haskell: You run multiple copies of the same binary on different machines, and you have the (#) operator to apply functions *on a remote machine*. So, for example, process (map f) # xs will serialize (map f) and send it over to some other machine. At that other machine, (map f) is deserialized and evaluated. In addition, two channels between the machines are opened: One for streaming the xs to that remote machine where the map is executed, and one for streaming the results back. The process and (#) operators have the following, rather harmless looking types: process :: (a - b) - Process a b (#) :: Process a b - (a - b) So no IO around, even if there is serialization and network communication going on. If you feel uncomfortable about that, you can use instantiate instead: instantiate :: Process a b - a - IO b And indeed, (#) is implemented in terms of instantiate and that unspeakable source of all false transparency: p # x = unsafePerformIO (instantiate p x) Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: ANNOUNCE zeno 0.1.0
Will Sonnex wrote: Zeno is a fully automated inductive theorem proving tool for Haskell programs. I tried it via the web interface, and it seems to be quite cool. Good work! However: You can express a property such as takeWhile p xs ++ dropWhile p xs === xs and it will prove it to be true for all values of p :: a - Bool and xs :: [a], over all types a, using only the function definitions. That is surprising, given that this property does not seem to be true for p = const undefined and xs /= []. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Most popular haskell applications
Ivan Lazar Miljenovic wrote: Bulat Ziganshin wrote: people, are you know haskell apps that has more than 50k downloads per month (or more than 25k users) ? Possible candidates: * GHC * XMonad * Darcs * Pandoc I have no idea how to measure number of downloads or users, but pandoc is used outside of the Haskell community. (And it can process this email). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell is a scripting language inspired by Python.
Hi, Albert Y. C. Lai wrote: I also invite you to play with my: http://www.vex.net/~trebla/humour/lmcify.html http://www.vex.net/~trebla/humour/lmcify.html?t=this+is+not+an+authorative+source. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid types fun
Hi, Mitar wrote: I would like to do that to remove repeating code like: from- newChan for- newChan let nerve = Nerve (Axon from) (AxonAny for) which I have to write again and again just to make types work out. Why I cannot move that into the function? One option is to write a little library of functions which create axons and nerves: newAxon :: Impulse i = IO (Axon (Chan i) i AxonConductive) newAxon = do chan - newChan return (Axon chan) newAxonAny :: IO (Axon (Chan i) AnyImpulse AxonConductive) newAxonAny = do chan - newChan return (AxonAny chan) newNoAxon :: Monad m = m (Axon (Chan i) i AxonNotConductive) newNoAxon = do return NoAxon newNerve :: Monad m = m (Axon a a' b) - m (Axon c c' d) - m (Nerve a a' b c c' d) newNerve newFrom newFor = do from - newFrom for - newFor return (Nerve from for) Note that newNerve does not take Axons, but rather monadic actions which create Axons. Now, you can use something like nerve - newNerve newAxon newAxonAny to create a concrete nerve. Tillmann PS. It might be an interesting exercise to use either liftM and liftM2 (from Control.Monad) or the ($) and (*) operators from Control.Applicative to implement these functions without do notation. PPS. Crosspost removed. I don't want to post to mailing lists which I do not read. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Edit Hackage
Ketil Malde wrote: Most web-based email archives seem to suck - where can we point to a nice URL to get an overview of a -cafe thread? http://thread.gmane.org/gmane.comp.lang.haskell.cafe/82667 Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Red links in the new haskell theme
Henning Thielemann wrote: If I enable JavaScript in Konqueror, I still see no style menu. However I would like to get it without JavaScript. It can certainly be achieved using a cookie. Both stylesheets are linked to from the text of the HTML files: link href=ocean.css rel=stylesheet type=text/css title=Ocean / link href=xhaddock.css rel=alternate stylesheet type=text/css title=Classic / Firefox uses this information to populate a menu (View | Stylesheet) with the following choices: - no style - Ocean - Classic No need for JavaScript or cookies. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Red links in the new haskell theme
Henning Thielemann wrote: Firefox uses this information to populate a menu (View | Stylesheet) with the following choices: - no style - Ocean - Classic No need for JavaScript or cookies. This would be optimal for me, if it would work this way. From the answers I understood that the style menu is something that is part of the document body, not something of the browser navigation toolset. Yes, the body of the document contains an additional style menu, so on well-behaving browsers, there are two style menus. See screenshot at http://www.informatik.uni-marburg.de/~rendel/style-menu.png Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type class design
Hi, Uwe Schmidt wrote: In the standard Haskell classes we can find both cases, even within a single class. Eq with (==) as f and (/=) as g belongs to the 1. case Note that the case of (==) and (/=) is slightly different, because not only can (/=) be defined in terms (==), but also the other way around. The default definitions of (==) and (/=) are mutually recursive, and trivially nonterminating. This leaves the choice to the instance writer to either implement (==) or (/=). Or, for performance reasons, both. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A new cabal odissey: cabal-1.8 breaking its own neck by updating its dependencies
Hi Paolo, Paolo Giarrusso wrote: - when recompiling a package with ABI changes, does cabal always update dependent packages? It never recompiles them. Recompilation should not be needed, because different versions of packages exports different symbols, so a package can never be linked against the wrong version of its dependency. However, see the following tickets: http://hackage.haskell.org/trac/hackage/ticket/701 http://hackage.haskell.org/trac/hackage/ticket/704 Interestingly, HTTP, directory, process, zip-archive were not reinstalled, which confirms that Cabal had reinstalled them before just because of an upgrade to the dependencies. I think you are misinterpreting this. When you asked cabal-install to install pandoc, it tried to make a consistent install plan for all its transitive dependencies. cabal-install will not touch a package which is not a transitive dependency of the package you request to be installed. Therefore, cabal-install will not touch Cabal if you ask it to install pandoc. To make a consistent install plan, cabal-install has to pick exactly one version number for each of the transitive dependencies, so that all version constraints of all transitive dependencies are fullfilled. For some reason, cabal-install picked old-locale-1.0.0.2 instead of the already installed old-locale-1.0.0.1, and newer versions of HTTP, directory etc. too. I think this is the bug: cabal-install should not be allowed to install old-locale, because doing so apparantly causes havoc. Looking at the inter-dependencies of pandoc's transitive dependencies, I do not see a reason to install a new version of a package instead of keeping the old. Maybe it's somehow related to the transition from base-3 to base-4? But I don't know how cabal-install decides which install plan to follow anyway. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A new cabal odissey: cabal-1.8 breaking its own neck by updating its dependencies
Hi Paolo, Paolo Giarrusso wrote: $ cabal install --dry cabal-install leksah-0.8.0.6 [... does not work ...] However, trying to install cabal-install and leksah separately works quite well. So do install them separately. cabal install p1 p2 is supposed to find a single consistent install plan for p1 and p2 and the transitive dependencies of either of them. This is useful if you plan to use p1 and p2 in a single project. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A new cabal odissey: cabal-1.8 breaking its own neck by updating its dependencies
Hi Paolo, Paolo Giarrusso wrote: cabal install p1 p2 is supposed to find a single consistent install plan for p1 and p2 and the transitive dependencies of either of them. This is useful if you plan to use p1 and p2 in a single project. Ahah! Then it's a feature. The need for consistency stems from a bug: in a tracker entry you linked to, http://hackage.haskell.org/trac/hackage/ticket/704, duncan argues that we also want to be able to do things like linking multiple versions of a Haskell package into a single application. I think this is a slightly different matter. Consider a package pair, which defines an abstract datatype of pairs in version 1: module Pair (Pair, fst, snd, pair) where data Pair a b = Pair a b fst (Pair a b) = a snd (Pair a b) = b pair a b = Pair a b In version 2 of pair, the internal representation of the datatype is changed: module Pair (Pair, fst, snd, pair) where data Pair a b = Pair b a fst (Pair b a) = a snd (Pair b a) = b pair a b = Pair b a Now we have a package foo which depends on pair-1: module Foo (foo) where import Pair foo = pair 42 '?' And a package bar which depends on pair-2: module Bar (bar) where import Pair bar = fst Now, we write a program which uses both foo and bar: module Program where import Foo import Bar main = print $ bar $ foo Even with the technical ability to link all of foo, bar, pair-1 and pair-2 together, I don't see how this program could be reasonably compiled. Therefore, I think that the notion of consistent install plans is relevant semantically, not just to work around some deficiency in the linking system. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] On to applicative
michael rice wrote: Prelude Data.Either let m = Just 7 Prelude Data.Either :t m m :: Maybe Integer So to create a value of type (Maybe ...), you can use Just. Prelude Data.Either let l = 2:[] Prelude Data.Either :t l l :: [Integer] So to create a value of type [...], you can use (:) and []. Prelude Data.Either let g = getLine Prelude Data.Either :t g g :: IO String So to create a value of type (IO ...), you can use getLine. Prelude Data.Either let e = Right abc Prelude Data.Either :t e e :: Either a [Char] So to create a value of type (Either ... ...), you can use Right. How can I similarly create an instance of (-) [...] ? An instance of (-) is usually called a function. And functions are created by lambda abstraction: Prelude let f = \x - x Prelude :t f f :: t - t So to create a value of type (... - ...), you can use \. Just like Either, - is a binary type constructor. Just like (Either a b) is a type, (a - b) is a type. And very much like you can create (Either a b) values with Left and Right, you can create (a - b) values with \. Tillmann PS. After studying how to construct values, it may be instructive to study how to take them apart. For example, Bool values can be taken apart by if-then-else expressions. What about Either, IO and - values? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unix emulation
Felipe Lessa wrote: I take it that the problem is that libcurl is a C library with a Unix-like build system, and that is the problem that needs Cygwin, right? One needs a compiler and libraries on the one hand, and a bunch of command-line tools on the other hand. On Windows, MinGW provides the former, while Cygwin provides a package manager to install the latter. MinGW seems to be bundled with the Haskell platform on Windows, so that should be ok. The Cygwin tools however have to be installed in addition to the Haskell platform, which is no big deal, but somewhat annoying. There are two steps to be done: (1) Install the core of Cygwin, and put it in the search path after the MinGW bundled with the Haskell platform. (2) If a cabal package fails to install because some tools (bash, perl, sed, make, ...) are missing, install the missing tool using the Cygwin package manager. So a cabal package is better suited for installation on Windows if it does not depend on any command-line tools for building (or operation, of course). In practice, that means that a portable Setup.hs should contain Haskell code, not system calls to command-line tools. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: philosophy of Haskell
Ertugrul Soeylemez wrote: let (x, world1) = getLine world0 world2 = print (x+1) world1 If between 'getLine' and 'print' something was done by a concurrent thread, then that change to the world is captured by 'print'. But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread. If print is not restricted to be a pure Haskell function, we don't need the world passing in the first place. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: philosophy of Haskell
Bulat Ziganshin wrote: But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread. the whole World includes any concurrent thread though ;) Oh I see. So given world1, print can simulate the behavior of the concurrent thread to take it into account when constructing world2. Since that simulation depends only on world1, print is still pure. Does that mean that world passing *does* account for concurrency after all? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: philosophy of Haskell
Brandon S Allbery KF8NH wrote:
I am confused by this discussion. I originally thought some time back that
IO was about world passing, but in fact it's just handing off a baton to
insure that a particular sequence of IO functions is executed in the
specified sequence and not reordered. Nothing in the baton is intended to
represent the actual state of the world, nor is anything said about
concurrent actions either in another thread of the current program or
elsewhere outside the program; only ordering of calls in the *current*
thread of execution.
That explains how the IO monad forces side-effecting functions into a
specified sequence, but this discussion is about how to understand what
these side-effecting functions do in a *pure* framework. So the idea is
to regard, for example, putStr as a pure function from a world state to
a different world state, assuming that the world state contains a String
which represents the contents of the terminal. We could then implement
and understand putStr in pure Haskell:
data World = World {
terminal :: String
...
}
type IO a = World - (World, a)
putStr :: String - World - (World, ())
putStr str world = (world {terminal = terminal world ++ str}, ())
The benefit of this point of view is that we can analyze the behavior of
putStr. For example, by equational reasoning, we could derive the
following equation:
putStr s1 putStr s2 == putStr (s1 ++ s2)
It seems that we can account for more features of IO by adding more
fields to the World record. This discussion is about whether we can
account for *all* of IO this way.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A GHC error message puzzle
Simon Marlow wrote: Really hClose shouldn't complain about a finalized handle, I'll see if I can fix that. That sounds like a work-around to me, not a fix, because it would not fix more complicated exception handlers. I don't think there's a problem with more complicated exception handlers. The fix is to make the finalized Handle look like a closed Handle; it's a fix to the finalizer, not the exception handler, so it's not a workaround for this one particular symptom. Given the documentation of bracket, I would expect the following to write to the file. main = bracket (openFile output WriteMode) (\handle - do hPutStr handle I want this to be written in any case hClose handle) blackhole blackhole = blackhole But currently, hPutStr complains about a finalized handle, and with your fix, it would complain about a closed handle, which is hardly better. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A GHC error message puzzle
Simon Marlow wrote: So what happens is this: - the recursive definition causes the main thread to block on itself (known as a black hole) - the program is deadlocked (no threads to run), so the runtime invokes the GC to see if any threads are unreachable - the GC finds that (a) the main thread is unreachable and blocked on a blackhole, so it gets a NonTermination exception (b) the Handle is unreachable, so its finalizer is started - the finalizer runs first, and closes the Handle - the main thread runs next, and the exception handler for writeFile tries to close the Handle, which has already been finalized Why is the Handle found unreachable? There seems to be a pointer to the Handle somewhere, which is later passed to the exception handler and used there. Why is that pointer not regarded by GC? Is that situation Handle-specific, or could step (b) above free memory the exception handler is going to acess? Really hClose shouldn't complain about a finalized handle, I'll see if I can fix that. That sounds like a work-around to me, not a fix, because it would not fix more complicated exception handlers. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] universal quantification is to type instantiations as existential quantification is to what
Hi, to understand forall and exists in types, I find it helpful to look at the terms which have such types. Joshua Ball wrote: mapInt :: forall a. (Int - a) - [Int] - [a] I can instantiate that function over a type and get a beta-reduced version of the type mapInt [String] :: (Int - String) - [Int] - [String] So mapInt could be defined with a upper-case lambda /\ which takes a type: mapInt = /\a - ... Of course, in Haskell, we don't have that lambda explicitly. The universal quantifier is basically a lambda, but it works at the type level instead of the value level. Not quite. It is the /\ which is like \, except that \ takes a value, while /\ takes a type. Now, the type of /\ ...is forall ..., and the type of \ ... is ... - ... . Therefore, forall is similar to -. And indeed, both forall and - describe terms which take arguments. However, there are two differences between - and forall. First, a term described by - takes a value argument, while a term described by forall takes a type argument. And second, the result type of a term described by - is independent from the argument taken, while the result type of a term described by forall may depend on the argument taken. My question is... what is the analog to an existential type? mapInt :: exists a. (Int - a) - [Int] - [a] This mapInt could be defined with a version of the pair constructor (,) which accepts a type in the first component. mapInt = (SomeType, ...) Note that the ... in that definition need to have the following type: (Int - SomeType) - [Int] - SomeType So exists is similar to (,). Both exists and (,) describe terms which represent pairs. And again, there are two differences between (,) and exists. First, a term described by (,) represents a pair of two values, while a term described by exists represents a pair of a type and a value. And second, the type of the second component of a term described by (,) is independent of the first component, while the type of the second component of a term described by exists may depend on the first component. 1. If I can instantiate variables in a universal quantifier, what is the corresponding word for variables in an existential quantifier? If foo has an universal type, the caller of foo can choose a type to be used by foo's body by instantiating the type variable. That type variable is available to foo's body. If foo has an existential type, the body of foo can choose a type to be available to the caller of foo by creating an existential pair. That type is available to foo's caller by unpacking the existential pair, for example, by pattern matching. 2. If type instantiation of a universally quantified variable is beta-reduction, what happens when existentially quantified variables are [insert answer to question 1]? beta-reduction happens when the type application meets the lambda abstraction: (/\ a - b) [T] ~ b [a := T] The corresponding reduction for existentials happens when the unpacking meets the construction of the existential pair. case (T, t) of (a, x) - b ~ b [a := T; x := t] I don't know how it is called. BTW, note how the type variable a is bound in the pattern of the case expression, so it scopes over b. But the type of b is also the type of the overall case expression. Therefore, if the type of b would mention the type variable a, so would the overall type of the case expression, and then, the type variable a would be used out of scope. This is why GHC complains about escaping type variables sometimes. 3. Is there any analogue to existential quantifiers in the value world? Forall is to lambda as exists is to what? Forall is to lambda as exists is to (,), as discussed above. HTH, Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: A GHC error message puzzle
Hi, the reading is not needed to make it happen. main = writeFile output blackhole where blackhole = blackhole In fact, writing is not needed either. main = bracket (openFile output WriteMode) hClose (\hdl - blackhole `seq` return ()) blackhole = blackhole Note that writeFile is indeed like this, so this seems to be the same problem. Sebastian Fischer wrote: Of course, the cause is the black hole. But why is it not reported? I guess the following happens: When the blackhole is detected in the third argument of bracket, the second argument is executed. But for some reason, the handle is already finalized at this point, so hClose raises an exception itself. But bracket reraises the exception from its third argument only if its second argument does not raise an exception itself. So in this case, the handle is finalized exception seems to eat the blackhole exception. So the question remains: Why is the handle finalized? (And what is finalizing an handle?) Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Accepting and returning polyvariadic functions
Will Jones wrote:
f :: Int - IO ()
f = undefined
g :: Int - Int - IO ()
g = undefined
h :: Int - Int - Int - IO ()
h = undefined
vtuple f :: IO (Int - (Int, ()))
vtuple g :: IO (Int - Int - (Int, (Int, (
I've tried to type vtuple using a type class; [...]
I've thought about it and it seems impossible to solve this problem
-- you keep needing to ``split'' the function type one arrow further on.
So you need to use recursion to handle the arbitrary deeply nested
arrows in the type of vtuple's argument. I tried it with type families,
but I don't see a reason why functional dependencies should not work.
{-# LANGUAGE FlexibleInstances, TypeFamilies #-}
module VTupleWithTypeFamilies where
We use two type families to handle the two places where the result type
of vtuple changes for different argument types.
type family F a
type family G a r
So the intention is that the type of vtuple is as follows.
class VTuple a where
vtuple :: a - IO (G a (F a))
The base case:
type instance F (IO ()) = ()
type instance G (IO ()) r = r
instance VTuple (IO ()) where
vtuple = undefined
And the step case:
type instance F (a - b) = (a, F b)
type instance G (a - b) r = a - G b r
instance VTuple b = VTuple (a - b) where
vtuple = undefined
A test case:
f :: Int - Bool - Char - Double - IO ()
f = undefined
test = do
vt - vtuple f
return (vt 5 True 'x' 1.3)
Testing it with ghci yields the following type for test, which looks
good to me.
test :: IO (Int, (Bool, (Char, (Double, ()
HTH, Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Can we come out of a monad?
Dan Doel wrote: But, to get back to BASIC, or C, if the language you're extending is an empty language that does nothing, then remaining pure to it isn't interesting. I can't actually write significant portions of my program in such a language, so all I'm left with is the DSL, which doesn't (internally) have the nice properties. I understand your argument to be the following: Functional languages are built upon the lambda calculus, so a *pure* functional language has to preserve the equational theory of the lambda calculus, including, for example, beta reduction. But since BASIC or C are not built upon any formal calculus with an equational theory, there is not notion of purity for these languages. I like your definition of purity, but I disagree with respect to your evaluation of BASIC and C. To me, they seem to be built upon the formal language of arithmetic expressions, so they should, to be pure arithmetic expression languages, adhere to such equations as the commutative law for integers. forall x y : integer, x + y = y + x But due to possible side effects of x and y, languages like BASIC and C do not adhere to this, and many other laws. I would therefore consider them impure. They could be more pure by allowing side effects only in statements, but not in expressions. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Couple of questions about *let* within *do*
michael rice wrote: OK, then there's also an implicit *in* after the *let* in this code. If you want to understand let statements in terms of let ... in ... expressions, you can do the following transformation: do s1 s2 let x1 = e1 x2 = e2 s3 s4 becomes do s1 s2 let x1 = e1 x2 = e2 in do s3 s4 So in a sense, there is an implicit in do. Must the implicit (or explicit) *in* actually use the calculated value(s)? No. By the way, note that lazy evaluation applies, so the expressions bound in the let may or may not be evaluated, depending on the rest of the program. And, the monad can continue on after the *let* (with or without the *in*) as below, i.e., the *let* needn't be the last statement in the *do*? Yes, there can be more statements after the let statement. In fact, the let statement must not be the last statement in the do-expression, because a do-expression has to end with an expression statement. Otherwise, what would the result of the do-expression be? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Suggestions For An Intro To Monads Talk.
Hi,
aditya siram wrote:
For example in the beginning it was useful for me to think of monads
(and typeclasses really) as approximating Java interfaces.
Type classes are somewhat parallel to Java interfaces, but Monad is a
*specific* type class, so it should be somewhat parallel to a *specific*
Java interface, if at all.
Type classes are somewhat parallel to Java interfaces because a Java
interface
interface Foo {
Result method (Argument argument);
}
declares that there is a set of types so that every type T in that set
has an operation (T, Argument) - Result, with these operations all
implemented specifically to particular type T. In Haskell, the type class
class Foo t where
method : t - Argument - Result
expresses a similar concept. There are a number of differences though:
Firstly, in Java, calls to the method are late bound, while in Haskell,
they are early bound. However, a kind of late bound behavior can be
achieved using existentials.
Secondly, in Java, the receiver of the method has to be of type T, and T
may not appear at other positions in the type of the method, while in
Haskell, T may appear anywhere in the type of the method, even more then
once.
Finally, in Java, T has to be a proper type (of kind *), while in
Haskell, it may be an improper type (of a kind involving -).
Already for the type class Functor, these differences become relevant.
class Functor f where
fmap :: (a - b) - f a - f b
f has kind (* - *), and it is mentioned twice in the type of fmap.
Conclusion: While Haskell type classes have some similarities to Java
interfaces, the type class Functor (or Monad, if you like) is not that
similar to any Java interface, because it uses features specific to
Haskell type classes which are not available in Java interfaces.
Nevertheless, it may be helpful for a Java developer to understand that
Haskell type classes are more similar to Java interfaces than to Java
classes.
Tillmann
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] can Haskell do everyting as we want?
Ivan Lazar Miljenovic wrote:: My understanding of tab-completion in IDEs for Java, etc. is that it just displayed every single possible class method for a particular object value, and then did some kind of matching based upon what you typed to narrow down the list, not that it was type-based. Good completion is type based. For example, consider the following situations in Eclipse: (1) int foo = bar.cursor here (2) String foo = bar.cursor here In both cases, completion will only propose methods of String and its super class Object, so the type of the receiver is taken into account. Furthermore, the proposed methods will be ordered differently in (1) and (2). In (1), the list of proposed methods starts with methods returning int, while in (2), the list of proposed methods starts with methods returning String, so the type of the context is taken into account. I guess that it may be easier to implement effective completion for Java because in Java, completion-relevant context information is often to the left of the completion position. On the other hand, shouldn't constraint-based type inference à la Haskell be relatively easy to extend towards type-based completion? An IDE could infer the types of the holes in half-finished source code, and then try to unify the types of identifiers in scope with the type of the hole the programmer is typing in. If the resulting constraint system is consistent, the identifier should be proposed as a completion. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Laziness question
michael rice wrote: f x = length [head x] g x = length (tail x) Wouldn't both functions need to evaluate x to the same level, *thunk* : *thunk* to insure listhood? There is no need to insure listhood at run time, since Haskell is statically typed. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can we come out of a monad?
C K Kashyap wrote: I am of the understanding that once you into a monad, you cant get out of it? That's not correct. There are many monads, including Maybe, [], IO, ... All of these monads provide operations (=), return and fail, and do notation implemented in terms of these functions, as a common interface. Using just this common interface, you cannot get out of the monad. But most if not all monads also provide additional operations, specific to the monad in question. Often, these operations can be used to get out of that monad. For example, with Maybe, you can use pattern matching: case do x - return 5 fail some message return (x + 3) of Just a - a Nothing - 0 So we can get out of many monads, but we need to know which one it is to use the appropriate operation. Kevin Jardine wrote: I'm still trying to understand how monads interact with types so I am interested in this as well. From my point of view, the most important fact about monads is: There is nothing special about monads! The type class Monad behaves like very other type class. A monadic type constructor behaves like every other type constructor. The type class methods (=), return and fail behave like every other type class method. There is nothing special about monads. The only speciality of monads is do notation, but do notation is only a syntactic convenience, and can be translated into calls of (=), return and fail, which, as noted above, are not special in any way. So, back to your question, since there is nothing special about monads, monads do not interact with types in any special way. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Can we come out of a monad?
Hi, I wrote: There is nothing special about monads! Kevin Jardine wrote: I've seen plenty of comments suggesting that monads are easy to understand, but for me they are not. My point was that monads are not a language feature whith special treatment of the compiler, but more like a design pattern or a standard interface, a way of using the language. There is no compiler magic about monads. Therefore, they can, in principle, be understand by reading their definition in Haskell. Nevertheless, I agree that it is hard to understand monads, because they are a clever way of using Haskell and use several of Haskell's more advanced features. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: lhs2TeX - lhs2TeX.fmt missing
Hi Ivan, (why are you answering off-list?) Ivan Miljenovic wrote: I was under the impression that with cweb, you can have one function definition split into two, with another completely different block of code in between them. I agree, that's something literate haskell can not do. (But it's different from what you wrote before). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] use of modules to save typing
Michael Mossey wrote: incrCursor :: State PlayState () Additional question: what is proper terminology here? Proper terminology for monadic things is somewhat debated. incrCursor is a monad This is not true. incrCursor is a monadic type incrCursor is not a type, so this can't be correct. However, incrCursor has a monadic type is somewhat reasonable. However, I would avoid it because it is quite vague. incrCursor is a monadic function incrCursor is a monadic computation These sound good to me. I would prefer the latter, because incrCursor does not take any arguments, so it is debatable whether it is a function. From my point of view, monadic functions should mean a function of type (a - m b) where m is a monad, i.e. arrows in a Kleisli category. An alternative to monadic computation would be monadic action. However, since we know which monad it is, I would prefer incrCursor is a state transformer or even incrCursor is a PlayState transformer. State is a monad State is a type constructor of a monad State is a monadic type None of these seem to be true. However, the following is: (State PlayState) is a monad. If you want to say something about State, maybe State is a parametric monad or State is a family of monads is appropriate. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
