Talk:Pointfree

There is a notion of "pointless" toposes. It seems to me that "pointfree" is related to this idea. Some explanation follows.

A topos is thought of as a model for set theory. Hence it is natural to calculate with "elements". A topos is also a model for sheaves on a space. In that case it is natural to calculate with "stalks". In either case, we associate (functorially) to each object of our category a set "made up of elements" and then do the calculation with these elements. There are "pointless" toposes (for example the Deligne-Barr topos) so one should learn to carry out topos theoretic calculations with the crutch of "elements" or "points".

kapil 02:06, 14 February 2009 (UTC)

Some combinators

I have found a serie of function combinators, which generalize (.) with pl. (The lambdabot plugin)

But I am not sure if it is interesting enough to add them to the page, I think they are, because they show some usage of pl, because it makes it possible to extract patterns, which you cant see, if you write it pointful.

On the other hand it adds a lot of noise to this page.

{-- Generalized function compositions. 
 - the stars represent the arity of the function on the left side. The pipes the arity of the function of the right side. 
 - The composite functions behave like f . g, only with more arguments. 
 - Eg: ((+) <**|> succ) 2 1 -> 4
 - --}


con :: (b1 -> b -> c) -> (a -> b1) -> b -> a -> c
con = (flip.) .(.)

{--Level operators. Heightens the arity of the function on the left. See for
   examples below. To heighten the arity of the function on the right you  simple add two combinators with the same arity of the function on the left. (<**|>.<**|>) = (<**||>)
   
--}

(<**>) :: (a -> b -> c) -> b -> a -> c
(<**>) = flip

(<***>) :: (a1 -> a -> b -> c) -> b -> a1 -> a -> c
(<***>) = con (<**>)

(<****>) :: (a2 -> a1 -> a -> b -> c) -> b -> a2 -> a1 -> a -> c
(<****>) = con (<***>)

(<*****>) :: (a3 -> a2 -> a1 -> a -> b -> c) -> b -> a3 -> a2 -> a1 -> a -> c
(<*****>) = con (<****>)


(<*****|>) :: (a1 -> a2 -> a3 -> a4 -> b -> c) -> (a -> b) -> a -> a1 -> a2 -> a3 -> a4 -> c
(<*****|>) = (<*|>).(<*****>)

(<****|>) :: (a1 -> a2 -> a3 -> b -> c) -> (a -> b) -> a -> a1 -> a2 -> a3 -> c
(<****|>) = (<*|>).(<****>)

(<***|>) :: (a1 -> a2 -> b -> c) -> (a -> b) -> a -> a1 -> a2 -> c
(<***|>) = (<*|>).(<***>)

(<**|>) :: (a1 -> b -> c) -> (a -> b) -> a -> a1 -> c
(<**|>) = (<*|>).(<**>)

(<*|>) :: (b -> c) -> (a -> b) -> a -> c
(<*|>) = (.)

(<*||>) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c
(<*||>) = (<*|>).(<*|>)

(<*|||>) :: (b -> c) -> (a -> a1 -> a2 -> b) -> a -> a1 -> a2 -> c
(<*|||>) = (<*|>).(<*||>)

(<*||||>) :: (b -> c) -> (a -> a1 -> a2 -> a3 -> b) -> a -> a1 -> a2 -> a3 -> c
(<*||||>) = (<*||>).(<*||>)

(<*|||||>) :: (b -> c) -> (a -> a1 -> a2 -> a3 -> a4 -> b) -> a -> a1 -> a2 -> a3 -> a4 -> c
(<*|||||>) = (<*|||>).(<*||>)


(<*||||||>) :: (b -> c) -> (a -> a1 -> a2 -> a3 -> a4 -> a5 -> b) -> a -> a1 -> a2 -> a3 -> a4 -> a5 -> c
(<*||||||>) = (<*|||>).(<*|||>)

(<**||>) :: (b -> a2 -> c) -> (a -> a1 -> a2) -> a -> a1 -> b -> c
(<**||>) = (<*||>).(<**>)
(<**|||>) :: (b -> a3 -> c) -> (a -> a1 -> a2 -> a3) -> a -> a1 -> a2 -> b -> c
(<**|||>) = (<*|>).(<**||>)
(<**||||>) :: (b -> a4 -> c) -> (a -> a1 -> a2 -> a3 -> a4) -> a -> a1 -> a2 -> a3 -> b -> c
(<**||||>) = (<*|>).(<**|||>)
(<***||>) :: (a2 -> a3 -> b -> c) -> (a -> a1 -> b) -> a -> a1 -> a2 -> a3 -> c
(<***||>) =  (<*||>).(<***>)

(<***|||>) :: (a3 -> a4 -> b -> c) -> (a -> a1 -> a2 -> b) -> a -> a1 -> a2 -> a3 -> a4 -> c
(<***|||>) = (<*|>).(<***||>)

--Edgarklerks 08:23, 20 May 2010 (UTC)

Discussion of partial applciation

I think it would be helpful to have the definition of (.) copied on the page for reference and to describe the technique of examples like (fn .).

--User:DougRansom February 18, 2012--