Re: [Haskell-cafe] Categorical description of systems with dependent types

2010-12-07 Thread Petr Pudlak
Hi, thanks to all who gave me valuable pointers to what to study. It will take me some time to absorb that, but it helped a lot. Best regards, Petr On Thu, Dec 02, 2010 at 02:25:41PM -0500, Dan Doel wrote: On Thursday 02 December 2010 10:13:32 am Petr Pudlak wrote: Hi, recently

[Haskell-cafe] Categorical description of systems with dependent types

2010-12-02 Thread Petr Pudlak
Hi, recently, I was studying how cartesian closed categories can be used to describe typed functional languages. Types are objects and morphisms are functions from one type to another. Since I'm also interested in systems with dependent types, I wonder if there is a categorical description

[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

2010-11-13 Thread Petr Pudlak
Hi Will, I was wondering, Zeno capable of proving just equational statements, or is it able to prove more general statements about programs? In particular, it would be interesting if Zeno would be able to prove that a function is total by verifying that it uses only structural

[Haskell-cafe] an evil type hangs GHC

2010-11-12 Thread Petr Pudlak
Hi, I was playing with the following example I found in D.A.Turner's paper Total Functional Programming: data Bad a = C (Bad a - a) bad1 :: Bad a - a bad1 b@(C f) = f b bad2 :: a bad2 = bad1 (C bad1) To my surprise, instead of creating a bottom valued function (an infinite loop), I

Re: [Haskell-cafe] an evil type hangs GHC

2010-11-12 Thread Petr Pudlak
On Fri, Nov 12, 2010 at 07:52:53PM +0100, Petr Pudlak wrote: Hi, I was playing with the following example I found in D.A.Turner's paper Total Functional Programming: data Bad a = C (Bad a - a) bad1 :: Bad a - a bad1 b@(C f) = f b bad2 :: a bad2 = bad1 (C bad1) To my surprise, instead

Re: [Haskell-cafe] Gödel' s System T

2010-11-11 Thread Petr Pudlak
Thanks Dan, the book is really interesting, all parts of it. It looks like I'll read the whole book. Best regards, Petr On Wed, Nov 10, 2010 at 05:21:16PM -0500, Dan Doel wrote: On Wednesday 10 November 2010 1:42:00 pm Petr Pudlak wrote: I was reading the paper Total Functional

[Haskell-cafe] Gödel's System T

2010-11-10 Thread Petr Pudlak
Hi, I was reading the paper Total Functional Programming [1]. I encountered an interesting note on p. 759 that primitive recursion in a higher-order language allows defining much larger set of function than classical primitive recursion (which, for example, cannot define Ackermann's

Re: [Haskell-cafe] Is let special?

2010-11-03 Thread Petr Pudlak
Hi Günther, from the semantical point of view, you can replace let x = e' in e by (\x - e) e' Both should evaluate to the same thing. However, from the typing point of view, it makes quite a difference. It is an integral part of the Hindley-Milner type inference algorithm, which is

Re: [Haskell-cafe] Pronouncing Curry and currying

2010-10-08 Thread Petr Pudlak
Best regards, Petr On Wed, Oct 06, 2010 at 01:23:39PM -0700, Donn Cave wrote: Quoth Petr Pudlak d...@pudlak.name, I have a question for native English speakers: What is the correct pronunciation of the name Curry (in Haskell Curry) and the derived verb currying? I found on Wikitonary

[Haskell-cafe] Pronouncing Curry and currying

2010-10-06 Thread Petr Pudlak
Hi all, I have a question for native English speakers: What is the correct pronunciation of the name Curry (in Haskell Curry) and the derived verb currying? I found on Wikitonary the name is (probably) of Irish orgin, so I suppose that the pronunciation may by nonstandard. Probably the best

[Haskell-cafe] Spell-checking lhs files

2010-09-30 Thread Petr Pudlak
Hi, recently I was spell-checking a literate Haskell source file (within the vim editor). The spell checker correctly ignored LaTeX commands, but I had to manually skip over code blocks inside |...|. This was really annoying and I couldn't figure out how to configure the spell checker to

Re: [Haskell-cafe] Coding conventions for Haskell?

2010-09-26 Thread Petr Pudlak
Hi Johan, On Sat, Sep 25, 2010 at 01:44:07PM +0200, Johan Tibell wrote: Quite a few people follow my style guide http://github.com/tibbe/haskell-style-guide/blob/master/haskell-style.md which codifies the style used in Real World Haskell, bytestring, text, and a few other libraries.

[Haskell-cafe] Coding conventions for Haskell?

2010-09-25 Thread Petr Pudlak
Hi, sometimes I have doubts how to structure my Haskell code - where to break lines, how much to indent, how to name functions and variables etc. Are there any suggested/recommended coding conventions? I searched a bit and I found a few articles and discussions: - Good Haskell coding

Re: [Haskell-cafe] OT: How a Common Lisp user views other programming languages

2010-01-26 Thread Petr Pudlak
On Thu, Jan 21, 2010 at 03:58:08PM -0800, Scott Michel wrote: Off topic, but funny: http://kvardek-du.kerno.org/2010/01/how-common-lisp-programmer-views-users.html ... This one is similar and IMHO even better: http://axgle.github.com/images/haskell.jpg -Petr

Re: [Haskell-cafe] a problem defining a monad instance

2009-11-08 Thread Petr Pudlak
On Fri, Nov 06, 2009 at 07:08:10PM +0100, Petr Pudlak wrote: Hi all, (This is a literate Haskell post.) I've encountered a small problem when trying to define a specialized monad instance. Maybe someone will able to help me or to tell me that it's impossible :-). To elaborate: I

[Haskell-cafe] Re: [Haskell] ANNOUNCE: GPipe-1.0.0: A functional graphics API for programmable GPUs

2009-10-07 Thread Petr Pudlak
Hi Tobias, (I'm completely new to GPU programming, so my question may be completely stupid or unrelated. Please be patient :-).) Some time ago I needed to perform some large-scale computations (searching for first-order logic models) and a friend told me that GPUs can be used to perform many

Re: [Haskell-cafe] funct.prog. vs logic prog., practical Haskell

2009-08-02 Thread Petr Pudlak
On Sun, Aug 02, 2009 at 08:36:27AM -0400, Carter Schonwald wrote: are you a student (undergrad or grad) or faculty (junior or senior)? These are all very different scenarios and accordingly different goals are realistic. I'm a faculty member (postdoc). I've been working in the field of

Re: [Haskell-cafe] funct.prog. vs logic prog., practical Haskell

2009-08-02 Thread Petr Pudlak
, albeit one with some restrictions related to everything impure. As a matter of course in such a class you would naturally also mention that there are languages such as haskell which lack such restrictions/ have clever ways around them. -Carter On Sun, Aug 2, 2009 at 8:52 AM, Petr Pudlak d

Re: [Haskell-cafe] excercise - a completely lazy sorting algorithm

2009-07-17 Thread Petr Pudlak
Hi all, I apologize that I didn't react to your posts, I was on a vacation. (BTW, if you ever come to Slovakia, I strongly recommend visiting Mala (Lesser) Fatra mountains. IMHO it's more beautiful than more-known Tatra mountains.) Thanks for your interest and many intriguing ideas. Especially,

[Haskell-cafe] an instance in other than the last type parameters

2009-07-17 Thread Petr Pudlak
Hi, I have probably a very simple question, but I wasn't able to figure it out myself. Consider a two-parameter data type: data X a b = X a b If I want to make it a functor in the last type variable (b), I can just define instance Functor (X a) where fmap f (X a b) = X a (f b) But how do

[Haskell-cafe] excercise - a completely lazy sorting algorithm

2009-07-06 Thread Petr Pudlak
Hi all, about a month ago, we were discussing sorting in Haskell with a friend. We realized a nice property of lazy merge-sort (which is AFAIK the implementation of Data.List.sort): Getting the first element of the sorted list actually requires O(n) time, not O(n * log n) as in imperative

Re: [Haskell-cafe] About the lazy pattern

2009-05-28 Thread Petr Pudlak
Hi Ryan, thanks for a nice and thorough explanation. I had trouble understanding the section of the tutorial as well. Maybe it would deserve to rewrite to something a bit simpler? Anyhow, I'd like to ask: Is there a reason for which pattern matching for single-constructor data types isn't lazy by

[Haskell-cafe] Haskell type system and the lambda cube

2009-05-24 Thread Petr Pudlak
Hi, I'm trying to get some better understanding of the theoretical foundations behind Haskell. I wonder, where exactly does Haskell type system fit within the lambda cube? http://en.wikipedia.org/wiki/Lambda_cube I guess it could also vary depending on what extensions are turned on. Thanks,

Re: [Haskell-cafe] Haskell type system and the lambda cube

2009-05-24 Thread Petr Pudlak
, whereas Haskell's Hindley-Milner type system is decidable. From this I get that Haskell's type system can't be one of the vertices of the cube. (BWT, will some future version of Haskell consider including some kind of dependent types?) Petr 2009/5/24 Petr Pudlak d...@pudlak.name: Hi, I'm

[Haskell-cafe] Functional Reactive Web Application Framework?

2009-05-13 Thread Petr Pudlak
Hi, I've been learning Haskell for a few months, and it has influenced my thinking about programs quite a lot. Most of my current work is creating complex web applications. Naturally, I was thinking about how to make rich internet applications (and GUI apps in general) in an (utmost :-))

Re: [Haskell-cafe] Functional Reactive Web Application Framework?

2009-05-13 Thread Petr Pudlak
On Wed, May 13, 2009 at 06:46:45AM -0400, Arjun Guha wrote: Flapjax is javascript so possibly there could be a way to integrate it into Haskell using HJavascript?  Maybe it could even be integrated into Happstack? The Flapjax compiler is written in Haskell, so that might help. I assume