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

[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, 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 of such systems. The problem (as I
see it) is that the codomain of a function depends on a value passed to
the function.

I'd happy if someone could give me some pointers to some papers or other
literature.


There are many different approaches to modelling dependent types in category
theory. Roughly, they are all similar to modelling logic, but they all differ
in details.

I think the easiest one to get a handle on is locally Cartesian closed
categories, although there's some non-intuitive stuff if you're used to type
theory. The way it works is this: a locally Cartesian closed category C is a
category such that all its slice categories are cartesian closed. This gets
you the following stuff:

---

Since C is isomorphic to C/1, where 1 is a terminal object, C is itself
Cartesian closed assuming said 1 exists. This may be taken as a defining
quality as well, I forget.

---

Each slice category C/A should be viewed as the category of A-indexed families
of types. This seems kind of backwards at first, since the objects of C/A are
pairs like (X, f : X -> A). However, the way of interpreting such f as a
family of types F : A -> * is that F a corresponds to the 'inverse image' of f
over a. So X is supposed to be like the disjoint union of the family F in
question, and f identifies the index of any particular 'element' of X.

Why is this done? It has nicer theoretical properties. For instance, A -> *
can't sensibly be a morphism, because * corresponds to the entire category of
types we're modelling. It'd have to be an object of itself, but that's
(likely) paradox-inducing.

---

Given a function f : B -> A, there's a functor f* : C/A -> C/B, which re-
indexes the families. If you think of this in the more usual type theory
style, it's just composition: B -f-> A -F-> *. In the category theoretic case,
it's somewhat more complex, but I'll just leave it at that for now.

Now, this re-indexing functor is important. In type theories, it's usually
expected to have two adjoints:

 Σf ⊣ f* ⊣ Πf

These adjoints are the dependent sum and product. To get a base type that
looks like:

 Π x:A. B

from type theory. Here's how we go:

 B should be A-indexed, so it's an object of C/A

 For any A, there's an arrow to the terminal object ! : A -> 1

 This induces the functor !* : C/1 -> C/A

 This has an adjoint Π! : C/A -> C/1

 C/1 is isomorphic to C, so C has an object that corresponds to Π!B, which is
 the product of the family B. This object is the type Π x:A. B

In general, ΠfX, with f : A -> B, and X an A-indexed family, F : A -> *, is
the B-indexed family, G : B -> * for ease, where G b = Π x : f⁻¹ b. F x. That
is, the product of the sub-family of X corresponding to each b. In the case of
B = 1, this is the product of the entire family X.

This adjointness stuff is (no surprise) very similar to the way quantifiers
are handled in categorical logic.

---

That's the 10,000 foot view. I wouldn't worry if you don't understand much of
the above. It isn't easy material. In addition to locally Cartesian closed
categories, you have:

 toposes
 hyperdoctrines
 categories with families
 contextual categories
 fibred categories

And I'm probably forgetting several. If you read about all of these, you'll
probably notice that there are a lot of similarities, but they mostly fail to
be perfectly reducible to one another (although toposes are locally Cartesian
closed).

I don't have any recommendations on a best introduction for learning this.
Some that I've read are:

 From Categories with Families to Locally Cartesian Closed Categories
 Locally Cartesian Closed Categories and Type Theory

but I can't say that any one paper made everything snap into place. More that
reading quite a few gradually soaked in. And I still feel rather hazy on the
subject.

Hope that helps some.

-- Dan


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 of such systems. The problem (as I 
see it) is that the codomain of a function depends on a value passed to 
the function.


I'd happy if someone could give me some pointers to some papers or other 
literature.


Thanks,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[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 
(inductive) recursion (on a well defined inductive type), i.e. each 
recursive function call must be on a syntactic subcomponent of its 
parameter. And dually, one might want to prove that a function is 
corecursive, meaning that each recursive call is guarded by a 
constructor.


Best regards,
Petr


Hi all,

My masters project Zeno was recently mentioned on this mailing list so
I thought I'd announce that I've just finished a major update to it,
bringing it slightly closer to being something useful. Zeno is a fully
automated inductive theorem proving tool for Haskell programs. 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.

Now that it's updated it can use polymorphic types/functions, and you
express properties in Haskell itself (thanks to SPJ for the
suggestion). It still can't use all of Haskell's syntax: you can't
have internal functions (let/where can only assign values), and you
can't use type-classed polymorphic variables in function definitions -
you'll have to create a monomorphic instance of the function -but I
hope to have these added reasonably soon. It's also still missing
primitive-types/IO/imports so it still can't be used with any
real-world Haskell code, it's more a bit of theorem proving "fun".

You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code
file given there has some provable properties about a few prelude
functions among other things.

Another feature is that it lists all the sub-properties it has proven
within each proof. When it verifies insertion-sort "sorted (insertsort
xs) === True" it also proves the antisymmetry of "<=" and that the
"insert" function preserves the "sorted" property.

Any suggestions or feedback would be greatly appreciated.

Cheers,

Will


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 of creating a bottom valued function (an 
infinite loop), I managed to send the GHC compiler (ver. 6.12.1) to 
an infinite loop. Could anybody suggest an explanation? Is this a GHC 
bug? Or is this "Bad" data type so evil that type checking fails?


   Thanks,
   Petr


PS: The following code compiles, the difference is just in modifying 
"bad2" to include an argument:



data Bad a = C (Bad a -> a)

bad1 :: Bad a -> a
bad1 b@(C f) = f b

bad2 :: (a -> a) -> a
bad2 f = bad1 (C $ f . bad1)


[BTW, "bad2" has the type of the Y combinator and indeed works as 
expected:



factorial :: (Int -> Int) -> Int -> Int
factorial _ 0 = 1
factorial r n = n * (r (n-1))

main :: IO ()
main = print $ map (bad2 factorial) [1..10]


... so one can get general recursion just by crafting such a strange 
data type.]


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] an evil type hangs GHC

[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 managed to send the GHC compiler (ver. 6.12.1) to an 
infinite loop. Could anybody suggest an explanation? Is this a GHC bug? 
Or is this "Bad" data type so evil that type checking fails?


Thanks,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 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 function). And that this is studied in in Gödel's System T.
It also states that this larger set of primitive functions includes all
functions whose totality can be proved in first order logic.

I was searching the Internet but I couldn't find a resource (a paper, a
book) that would explain this in detail, give proofs etc. I'd be happy
if someone could give me some directions.


Girard's book, Proofs and Types, has some stuff on System T. A translation is
freely available:

 http://www.paultaylor.eu/stable/Proofs+Types.html

Skimming, it looks like he gives an argument that T can represent all
functions that are provably total in Peano arithmetic.

The rest of the book is also excellent.

-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 function). And that this is studied in in Gödel's System T. 
It also states that this larger set of primitive functions includes all 
functions whose totality can be proved in first order logic.


I was searching the Internet but I couldn't find a resource (a paper, a 
book) that would explain this in detail, give proofs etc. I'd be happy 
if someone could give me some directions.


Thanks,
Petr

[1] 
http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Is "let" special?

[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 used by many functional languages. Consider the following two 
expressions:



f = (\x -> x x) (\y -> y)
g = let x = \y -> y in x x


The function "f" is not typable in the Hindley-Milner type system, while 
"g" is is (and its type is "a -> a"). The reason is that in the first 
case (f), the typing system tries to assign a single type to "x", which is 
impossible (one would have to unify types "a" and "a -> b"). In the 
second case (g), the typing system assigns "x" a polymorphic type schema

  forall a.a -> a
which can be instantiated to both "a -> a" (the second "x") and "(b -> 
b) -> (b -> b)" (the first "x"), and then applied together. I'd say that 
"let ... in ..." is a core feature of the language that gives us 
parametric polymorphism.


If you are interested in the details, I'd suggest you to read the 
original paper [damas1982principal].


Best regards,
Petr

@conference{damas1982principal,
  title={{Principal type-schemes for functional programs}},
  author={Damas, L. and Milner, R.},
  booktitle={Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles 
of programming languages},
  pages={207--212},
  year={1982},
  organization={ACM},
  url   =   
{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.122.3604&rep=rep1&type=pdf}
}

On Tue, Nov 02, 2010 at 02:34:29AM +0100, Günther Schmidt wrote:

Hi all,

is there something special about "let"? I don't mean only its use in 
haskell, but in the general context of programming languages.


I've been given a few hints over time when I asked question 
concerning DSLs but regretfully didn't follow them up.


Günther

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Pronouncing "Curry" and "currying"

[Petr Pudlak]

Hi,

thanks for both the explanation (Donn) and the sound sample (Luke). 
Unfortunately, "hurry" is pronounced differently in British and US 
English [1], so again I was a little bit confused :-). But Luke's sound 
sample made it clear for me.


[1] http://en.wiktionary.org/wiki/hurry#Pronunciation

  Best regards,
  Petr

On Wed, Oct 06, 2010 at 01:23:39PM -0700, Donn Cave wrote:

Quoth Petr Pudlak ,


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.


I'm going to vote for `rhymes with hurry(ing).'  Stress on the first
syllable, where the vowel is mid-position and unrounded, the null
vowel that's often spelled 'u'.  My Irish neighbor might pronounce
it a little different - more like Car-y - but he's kind of hard to
understand, so I wouldn't take him as an example!

Is that nonstandard?  I don't know - is there a standard?  The only
one I know is that for any English name, the main stress falls on
the first syllable.  (I think even including Gaelic origins, but
of course not counting Mac/Mc/O prefixes.)  The only exception
I can think of is that most people with the Scottish name Monroe
seem to put the stress on the second syllable.

Donn
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Pronouncing "Curry" and "currying"

[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 way to answer would be either a link to some voice 
sample or written using some standard phonetic alphabet.


Thanks a lot,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Spell-checking lhs files

[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 
skip over code. Does anybody have a solution for that?


Thanks a lot,
Petr


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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.


Thanks for sharing the link, it's quite helpful. It's just what I was 
looking for. 

One more thought: Do you also have some recommendations for formatting 
'let ... in ...' expressions?


 Best regards,
 Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Coding conventions for Haskell?

[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 standards from Stackoverflow
  http://stackoverflow.com/questions/1983047/good-haskell-coding-standards
- Programming guidelines from Haskellwiki
  http://www.haskell.org/haskellwiki/Programming_guidelines
- How to read Haskell from Haskellwiki (this is actually about reading, 
  not composing code, but still worth reading)

  http://www.haskell.org/haskellwiki/How_to_read_Haskell
- Good Haskell Style
  http://urchin.earth.li/~ian/style/haskell.html

but they usually address only a few specifics. I was looking for 
something more complete and comprehensive. Perhaps something like Java 
has [1].  Any suggestions?


Best regards,
Petr

[1] http://www.oracle.com/technetwork/java/codeconv-138413.html
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Petr Pudlak]

Hi,

thanks to all for all the helpful answers and references. Maybe I'll try
to collect them into a wiki page, if I have time. It looks like that I'm
not the only one facing this problem and many people know different
tricks how to handle it.

Yes, I was thinking about using lists of pairs instead of Maps. But
since I expect to have just a little distinct elements, but many >>=
operations, lists would probably grow to an enormous sizes, while Maps
will remain quite small.

The most intriguing idea for me was wrapping my pseudo-monad into the
continuation monad. I didn't have time to think it over, but I wondered
if the same (or similar) trick could be used to applicative functors
(which are not monads) or arrows.

(I found out that J. Hughes faced a similar problem in his paper
"Programming with Arrows" (p.42), but not with monads but arrows.)

Now I can enjoy playing with probabilities :-). Maybe having complex
numbers instead of Floats in the Distrib type would be a nice way how to
simulate (at least some) quantum computations.

RMonad also seems quite promising, and it looks like a more general
solution, but I had no time to try it out yet.

With best regards,
Petr

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 wanted to define a data type which is a little bit
> similar to the [] monad. Instead of just having a list of possible
> outcomes of a computation, I wanted to have a probability associated
> with each possible outcome.
> 
> A natural way to define such a structure is to use a map from possible
> values to numbers, let's say Floats:
> 
> > module Distribution where
> > 
> > import qualified Data.Map as M
> > 
> > newtype Distrib a = Distrib { undistrib :: M.Map a Float }
> 
> Defining functions to get a monad instance is not difficult.
> "return" is just a singleton:
>  
> > dreturn :: a -> Distrib a
> > dreturn k = Distrib (M.singleton k 1)
> 
> Composition is a little bit more difficult, but the functionality is
> quite natural. (I welcome suggestions how to make the code nicer / more
> readable.) However, the exact definition is not so important.
> 
> > dcompose :: (Ord b) => Distrib a -> (a -> Distrib b) -> Distrib b
> > dcompose (Distrib m) f = Distrib $ M.foldWithKey foldFn M.empty m
> >   where
> >  foldFn a prob umap = M.unionWith (\psum p -> psum + prob * p) umap 
> > (undistrib $ f a)
> 
> The problem is the (Ord b) condition, which is required for the Map
> functions.  When I try to define the monad instance as
> 
> > instance Monad Distrib where
> > return = dreturn
> > (>>=)  = dcompose
> 
> obviously, I get an error at (>>=):
> Could not deduce (Ord b) from the context.
> 
> Is there some way around? Either to somehow define the monad, or to
> achieve the same functionality without using Map, which requires Ord
> instances?
> 
> Thanks a lot,
> Petr
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Approaches to dependent types (DT)

[Petr Pudlak]

Hi Pat,

you might be interested in Agda [1] and the tutorial "Dependently Typed
Programming in Agda" [2]. I'm just reading the tutorial and it helps me
a lot with understanding the concept.

Also if you'd like to have a deeper understanding of the underlying
theory, I'd suggest reading Barendregt's "Lambda Calculi with Types"
[3].

Best regards,
  Petr

[1] http://wiki.portal.chalmers.se/agda/
[2] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
[3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391
and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z

On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
> Hi,
> I am trying to understand the concept of dependent types as described in
> Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am
> particularly interested in understanding two flavours of dependency
> mentioned by Hinze et al:
> 1) Types depending on values called dependent types
> 2) Types depending on types called parametric and type-indexed types
> 
> I think that ascending levels of abstraction are important here: values
> - types - classes (Hallgren 2001). Here is a Haskell example of the use
> of DT:
> 
> class Named object name | object -> name where
> name :: object -> name
> 
> instance (Eq name, Named object name) => Eq object where
> object1 == object2 = (name object1) == (name object2)
> 
> I think that the intended semantics are:
> 1) Objects have names  and can be compared for equality using these names.
> 2) Two objects are considered equal (identical) if they have the same name.
> 3) The type of a name depends on the type of the object, which gets
> expressed as a type dependency (object -> name).
> I am not sure about the last semantic it might be interpreted as "the
> named object depends on..". This may indicate a flaw in my understanding
> of DT.
> 
> I am aware that dependent types can be used to express constraints on
> the size of lists and other collections. My understanding of Haskell's
> functional dependency is that object -> name indicates that fixing the
> type object should fix the type name (equivalently we could say that
> type name depends on type object). The class definition seems to show a
> *type-to-type* dependency (object to name), while the instance
> definition shows how a name value is used to define equality for objects
> which could be interpreted as a *value-to-type* dependency (name to
> object) in the opposite direction to that of the class.
> 
> My questions are:
> Question 1: Is my understanding correct?
> Question 2: What flavour of DT is this does this example exhibit?
> 
> Best regards,
> Pat
> 
> 
> Hallgren, T. (2001). Fun with Functional Dependencies. In the
> Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
> 2001.
> Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
> Programming in Haskell. Datatype-generic programming: international
> spring school, SSDGP 2006.
> 
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 simple computations in parallel. Could GPipe
be used for such a task? I.e. to program some non-graphical,
parallelized algorithm, which could be run on a GPU cluster?

Thanks for your answer,

Petr

On Sun, Oct 04, 2009 at 08:32:56PM +0200, Tobias Bexelius wrote:
> I'm proud to announce the first release of GPipe-1.0.0: A functional graphics
> API for programmable GPUs.
>  
> GPipe models the entire graphics pipeline in a purely functional, immutable
> and typesafe way. It is built on top of the programmable pipeline (i.e.
> non-fixed function) of OpenGL 2.1 and uses features such as vertex buffer
> objects (VBO's), texture objects and GLSL shader code synthetisation to create
> fast graphics programs. Buffers, textures and shaders are cached internally to
> ensure fast framerate, and GPipe is also capable of managing multiple windows
> and contexts. By creating your own instances of GPipes classes, it's possible
> to use additional datatypes on the GPU.
>  
> You'll need full OpenGL 2.1 support, including GLSL 1.20 to use GPipe. Thanks
> to OpenGLRaw, you may still build GPipe programs on machines lacking this
> support.
>  
> The package, including full documentation, can be found at:
> http://hackage.haskell.org/package/GPipe-1.0.0
>  
> Of course, you may also install it with:
> cabal install gpipe
>  
>  
> Cheers!
> Tobias Bexelius
> 
> ━━
> kolla in resten av Windows LiveT. Inte bara e-post - Windows LiveT är mycket
> mer än din inkorg. Mer än bara meddelanden
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Petr Pudlak]

That's actually a good idea. I haven't considered this alternative so far,
probably because I have always been working with first-order theorem provers.
But I guess eventually I'll merge my interests in ATP and FP and start doing
some serious work with higher-order theorem provers like coq or Isabelle.

Petr

On Sun, Aug 02, 2009 at 09:03:14AM -0400, Carter Schonwald wrote:
> Have you considered say proposing a class on theorem proving that uses coq?
> www.coq.inria.fr . Such a class would entail teaching how to program using the
> coq term language, which is itself a pure functional language, 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  wrote:
> I'm a faculty member (postdoc). I've been working in the field of
> automated
> theorem proving, but for about a year I'm also very interested in Haskell
> and
> in general in the theory behind functional languages. Since I find FP to
> be a
> very important programming concept, I'd like to achieve that we start
> teaching
> it at the university.
> 
> Petr
> 
> 
> 
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 automated
theorem proving, but for about a year I'm also very interested in Haskell and
in general in the theory behind functional languages. Since I find FP to be a
very important programming concept, I'd like to achieve that we start teaching
it at the university.

Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Petr Pudlak]

Hi all,

I'd like to convince people at our university to pay more attention to
functional languages, especially Haskell. Their arguments were that

(1) Functional programming is more academic than practical.
(2) They are using logic programming already (Prolog); why is Haskell
better than Prolog (or generally a functional language better than a
logic programming language)?

(1) is easier to answer, there are a lots of applications at HaskellWiki, or
elsewhere around the Internet, written in Haskell, OCaml, etc.  Still, I
welcome comments on your experience, for example, if you have written some
larger-scale application in Haskell (or another a functional language) that is
not at HaskellWiki, and perhaps if/why you would recommend doing so to other
people.

(2) is harder for me, since I've never programmed in Prolog or another language
for logic programming. I'd be happy if anyone who is experienced in both Prolog
and Haskell could elaborate the differences, pros & cons etc.

Thanks,
Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 I write it if I want X to be a functor in its first type variable?
Is that possible at all?
Something like:

> instance Functor ??? where
> fmap f (X a b) = X (f a) b

Thanks in advance,
  Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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, I like
cata-/ana-/hylo-morphisms, it looks to me as a very useful concept to learn.

I hope I'll manage to create my own version of the sorting algorithm based on
your advices. Maybe I'll also try to do some real benchmarks, if I have time.

-Petr

On Tue, Jul 07, 2009 at 02:49:08AM +0200, Matthias Görgens wrote:
> The "sorted array of bags of unsorted input" is a nice idea.  However,
> you have to use the data structure in a single-threaded [1] fashion to
> obtain the claimed bounds.
> 
> Here's a pure solution that uses amortization and laziness.
> 
> > import qualified Data.Sequence as S
> > import Data.Sequence ((><))
> > import Data.Foldable
> > import Data.Monoid
> 
> Suppose we have a function to find the the median of a list, and
> partition it into three sublists: Smaller than the median, equal to
> the media, larger than the median.  That function should run in linear
> time.
> 
> > partitionOnMedian :: forall a. (Ord a) => (S.Seq a) -> BTreeRaw a (S.Seq a)
> 
> where the following data structure holds the sublists and some
> bookkeeping information:
> 
> > data BTreeRaw a m = Leaf
> >   | Node {cmp::(a->Ordering)
> >  , lN :: Int
> >  , less::m
> >  , eq :: (S.Seq a)
> >  , gN :: Int
> >  , greater::m
> >  }
> 
> where 'lN' and 'gN' are the length of 'less' and 'greater'.
> 
> We can make BTreeRaw a functor:
> 
> > instance Functor (BTreeRaw a) where
> > fmap f Leaf = Leaf
> > fmap f (Node c lN l e gN g) = Node c lN (f l) e gN (f g)
> 
> Now using a fixed-point construction we can bootstrap a sorting
> algorithm from partitionOnMedian:
> 
> > data Fix m = Fix {unfix :: (m (Fix m))}
> > type BTree a = Fix (BTreeRaw a)
> 
> > treeSort :: forall a. (Ord a) => S.Seq a -> BTree a
> > treeSort = Fix . helper . partitionOnMedian
> > where helper = fmap (Fix . helper . partitionOnMedian)
> 
> Now treeSort produces the thunk of a balanced binary search tree.  Of
> course we can get a sorted list out of it (forcing the whole
> structure):
> 
> > flatten :: BTree a -> S.Seq a
> > flatten (Fix Leaf) = S.empty
> > flatten (Fix (Node _ lN l e gN g)) = flatten l >< e >< flatten g
> 
> > mySort = flatten . treeSort
> 
> But we can also get elements efficently, forcing only a linear amount
> of comparisions in the worst case:
> 
> > index :: BTree a -> Int -> a
> > index (Fix Leaf) _ = error "tried to get an element of Leaf"
> > index (Fix (Node lN l e gN g)) i | i < lN
> >  = index l i
> >  | i - lN < S.length e
> >  = S.index e (i-lN)
> >  | i - lN - S.length e < gN
> >  = index g (i - lN - S.length e)
> >  | i - lN - S.length e - gN >= 0
> >  = error "index out of bounds"
> 
> Although we do have to force comparisions only once every time we
> touch the same element in the tree, we do still have to traverse the
> tree (in logarithmic time).
> 
> If you want linear time access on first touch of an element and
> constant time access afterwards us toArray:
> 
> > toArray :: (IA.IArray a t) => Fix (BTreeRaw t) -> a Int t
> > toArray tree = IA.listArray (0,maxI) (map (index tree) [0..maxI])
> > where size (Fix Leaf) = 0
> >   size (Fix (Node lN _ e gN _)) = lN + S.length e + gN
> >   maxI = size tree - 1
> 
> [1] Single-Threaded in the sense of Okasaki's use of the word.
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 languages. And
immediately we asked: Would it be possible to create a lazy selection/sorting
algorithm so that getting any element of the sorted list/array by its index
would require just O(n) time, and getting all the elements would still be in
O(n * log n)?

More precisely: The result of sorting an n-element list or array should be a
structure that allows to ask i-th element of the result (for example, a lazy
array). Asking k arbitrary elements should take no more than
  O(min(n * log n, k * n))

I believe that this could be done, but so far I wasn't able to implement and
show it myself. I think the solution would be somewhat modified lazy quicksort
(or "Median of Medians algorithm" if we want to be sure that we get good
pivots).

Perhaps somebody else would also like to give it a try? Or perhaps explain me
why it's not possible?

Best regards,
Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] About the lazy pattern

[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 default? For example, why do I have
to write

> weird ~(x,y) = (1,x)
> crazy = weird crazy

when the compiler knows that the type (x,y) has just the single constructor,
and could automatically introduce the additional laziness without any risk?

Petr

> Hi nemo.  I had a lot of trouble with that section of the tutorial as
> well, and I believe that once you get it, a lot of Haskell becomes a
> lot simpler.
> 
> The way I eventually figured it out is using this idealized execution
> model for Haskell: you just work by rewriting the left side of a
> function to its right side.  The only question is figuring out *which*
> function to rewrite!
> 
> Here's a simpler example:
> 
> > f 0 = 0
> > f x = x+1
> 
> > g (x:xs) = error "urk"
> > g [] = 2
> > const a b = a
> 
> > ex1 = const (f 1) (g [2,3])
> > ex2 = f (const (g []) (g [1,2]))
> 
> Lets say you wanted to know the value of ex1; you just use rewriting
> 
> ex1
> -- rewrite using ex1
> = const (f 1) (g [2,3])
> -- rewrite using const
> = f 1
> -- rewrite using f (second pattern)
> = 1+1
> -- rewrite using +
> = 2
> 
> But lets say we picked a different order to rewrite...
> 
> ex1
> -- rewrite using ex1
> = const (f 1) (g [2,3])
> -- rewrite using g
> = const (f 1) (error "urk")
> -- rewrite using error
> computation stops
> 
> Of course this is bad, and it was obviously wrong to evaluate g first
> (because const is lazy).  So one heuristic we always use is "rewrite
> the leftmost application first" which avoids this problem.  But lets
> try that rule on ex2!
> 
> ex2
> -- rewrite using ex2
> = f (const (g []) (g [1,2]))
> -- rewrite using f
> = ?
> 
> Unfortunately, now we don't know which pattern to match!  So we have
> to pick a different thing to rewrite.  The next rule is that, if the
> thing you want to rewrite has a pattern match, look at the argument
> for the patterns being matched and rewrite them instead, using the
> same "leftmost first" rule:
> 
> f (const (g []) (g [1,2]))
> -- trying to pattern match f's first argument
> -- rewrite using const
> = f (g [])
> -- still pattern matching
> -- rewrite using g
> = f 2
> -- now we can match
> -- rewrite using f (second pattern)
> = 2+1
> -- rewrite using +
> = 3
> 
> So, back to the original question (I'm rewriting the arguments to
> "client" and "server" for clarity)
> 
> > reqs = client init resps
> > resps = server reqs
> > client v (rsp:rsps) = v : client (next rsp) rsps
> > server (rq:rqs) = process rq : server rqs
> 
> Lets say we are trying to figure out the value of "resps", to print
> all the responses to the screen:
> 
> resps
> -- rewrite using resps
> = server reqs
> -- pattern match in server
> -- rewrite reqs
> = server (client init resps)
> -- pattern match in server
> -- pattern match also in client
> -- rewrite using resps
> = server (client init (server reqs))
> -- pattern match in server, client, then server
> -- rewrite using reqs
> = server (client init (server (client init resps)))
> 
> You see that we are in a loop now; we are stuck trying to pattern
> match and we will never make any progress!
> 
> The "lazy pattern" says "trust me, this pattern will match, you can
> call me on it later if it doesn't!"
> 
> > reqs = client init resps
> > resps = server reqs
> > client v (rsp:rsps) = v : client (next rsp) rsps
> > server (rq:rqs) = process rq : server rqs
> 
> resps
> -- rewrite resps
> = server reqs
> -- server wants to pattern match, rewrite reqs
> = server (client init resps)
> -- Now, the lazy pattern match says "this will match, wait until later"
> -- rewrite using client!
> = let (rsp:rsps) = resps
>in server (init : client (next rq) rqs)
> -- rewrite using server
> = let (rsp:rsps) = resps
>in process init : server (client (next rq) rqs)
> 
> We now have a list node, so we can print the first element and
> continue (which requires us to know the code for "process" and "next",
> but you get the idea, I hope!)
> 
> Now of course, you can lie to the pattern matcher:
> 
> > next x = x + 1
> > init = 5
> 
> client init []
> -- rewrite using client
> = let (rsp0:rsps0) = []
>in init : client (next rsp0) rsps0
> -- rewrite using init
> = let (rsp0:rsps0) = []
>in 5 : client (next rsp0) rsps0
> 
> -- print 5 and continue to evaluate...
>let (rsp0:rsps0) = []
>in client (next rsp0) rsps0
> -- rewrite using client
> = let
> (rsp0:rsps0) = []
> (rsp1:rsps1) = rsps0
>in (next rsp0) : client (next rsp1) rsps1
> -- rewrite using next
> = let
> (rsp0:rsps0) = []
> (rsp1:rsps1) = rsps0
>in rsp0+1 : client (next rsp1) rsps1
> -- + wants to "pattern match" on its first argument
> -- rewrite using rsp0
> computation stops, pattern match failure

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

[Petr Pudlak]

On Sun, May 24, 2009 at 12:18:40PM +0400, Eugene Kirpichov wrote:
> Haskell has terms depending on types (polymorphic terms) and types
> depending on types (type families?), but no dependent types.

But how about undecidability? I'd say that lambda2 or lambda-omega have
undecidable type checking, 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 :
> > 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, Petr
> > ___
> > Haskell-Cafe mailing list
> > Haskell-Cafe@haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> 
> 
> 
> -- 
> Eugene Kirpichov
> Web IR developer, market.yandex.ru
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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? 
I guess it could also vary depending on what extensions are turned on.

Thanks, Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[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 you want to write FRP in a Haskell-embedded DSL and generate
> FRP'd JavaScript.  If you wish to use Flapjax as a supporting library
> I'd be glad to help.
> 
> Arjun

Actually, I wanted to use Flapjax as the base for client-side programming.
I didn't think about combining Flapjax with HJavaScript, this is quite a good
idea.

However, this would is just one part of what I'd like to have. No doubt many
things can be done on the client, but more serious work or database
operations must be done on the server anyway. Ideally, I'd like to spare a
programmer from:
 * Working with HTML (unless explicitly desired); Instead, I'd prefer to
   compose the pages from components, either predefined or user-defined. This
   could be done for example using DSL in Haskell. The components could be both
   lightweight (almost HTML), or heavyweight like "menu", "toolbar" etc.
 * Transferring data between a server/client. Especially using FRP, this might
   be done very neatly I suppose. An event stream or a behavior could be
   transferred seamlessly by the framework from the client to the server and
   vice versa.  The programmer would only see behaviors on either side.

I've been working with the ZK framework  lately, and it has
many nice features. For example, composing pages from high-level components,
the possibility to separate the layout of the pages form the controlling
code, or sparing a programmer from working with HTML and HTTP requests -
everything is done just by manipulating component objects and handling
events. However, it's not functional at all. I believe FRP would be much better
solution than classical event handling. And secondly, it's in Java, which is
nothing bad (actually my code is in Scala), just it's not Haskell.

Happsstack looks good, though I didn't have time to study it.

Thanks for the links for OCAML JavaScript FRP, it looks iteresting too.

Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Functional Reactive Web Application Framework?

[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 :-)) functional
way. Recently I found out the concepts of functional reactive programming
, which
supersede and generalize my ideas. My question is:

"Is there a FRP web application framework,
 or perhaps an effort to create one?"

If not, I'd be willing to start such a project, but since I'm not very
experienced Haskell programmer, I'd most likely need some help from somebody
more experienced. If somebody would be interested, my ideas go as follows:


Handling events in GUI/RIA applications can be very tedious, especially for
complex applications. Instead, I'd prefer something like that:

1) Abstract what a user wants to see using a structured datatype,
   specifically tailored for the application. You may imagine it as something
   like a structured URL. This can be then viewed as a FRP behavior --
   a function of the user's request depending on time.
2) The data that will be displayed on the page are a function of this
   structured user request and an environment, which is usually database. This
   is again a behavior.
3) Finally, the resulting page is a function of the data (again a behavior).
4) User actions that change the application state (update the database) could
   be viewed as FRP events.

So instead of handling tons of events, the programmer would construct the
application mostly by composing behaviors. Only state-changing user actions
would be handled as events.

Does anybody see these ideas as useful? Constructive criticism is welcomed.

Best regards,
Petr
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe