🚀 go-pugleaf

A ``real'' third-order function:

A real number can be represented by a first order function

	integer -> integer

or 

	integer -> rational

Functions from reals to reals are therefore second order, and
so a function which integrates a real function over an interval 
is third order:

	(real -> real) -> real -> real -> real

Simon Thompson

Simon Thompson				e-mail:	sjt@ukc.ac.uk
Computing Laboratory			phone:	+44-227-764000 extn. 3820
University of Kent			fax:	+44-227-762811
Canterbury, Kent,
CT2 7NF, UK

In article <BvFvEz.7A@dcs.ed.ac.uk> alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:

   However, I find it quite hard to come up with useful examples of 3rd
   order functions (e.g. which have types like ((A->B)->C)->D).

   Sure, it is not hard to come up with constructed examples like:

	   \lambda f:(A->A)->B . f (\lambda  x:A . x) : ((A->A)->B)->B

   but I am rather looking for examples motivated by programming
   problems. 

   Any ideas?

Check out microwave and analog engineering.  Information is passed as
"signals", or functions from time (or frequency) to some other
physical quantity, such as voltage, current, or power.  The function
of various devices is expressed as a function on these signals; for
example, in the simple case, a mixer will take two functions and
produce a function which is their sum.

As this gets more complex (for example, writing a general description
which produces behaviors based upon parameters such as gain and power
consumption), third order functions appear frequently.

					Dave Barton
					dlb@hudson.wash.inmet.com

In article <1992Oct1.174259@cs.utwente.nl> ramaer@cs.utwente.nl (Mark Ramaer) writes:

   "alt" chooses between two "a"-parsers.

   > alt :: ([t]->Bool) -> Parser t r a -> Parser t r a -> Parser t r a
   > alt test aa bb = \contin input ->
   >       if test input
   >	then aa contin input
   >       else bb contin input

   > sequenceOption :: ([*]->bool) -> Parser t r a -> Parser t r [a]
   > sequenceOption test aa = alt test (sequence test aa) (empty [])

   "Parser t r a" is a 2nd order type, so "alt" and "sequenceOption"
   are 3rd order functions.

Thanks Mark, this certainly is a 3rd order function. In another
posting I tried to make the requirements more precise:

   If we have polymorphism, it is not clear what level to assign to type
   variables. In fact it is quite easy to get a 3rd order functions just
   by instantiating the type of polymorphic map by a 1st order function
   type for the input list. However, I am interested in *genuine* higher
   order functions, i.e. which do not show up as instantiations of
   polymorphic functions. This means that in this context I consider the
   order of a type variable as 0.

Your function alt can be obtained by instantiating a 2nd order
polymorphic function to the type Parser, right? In this way it is not
genuinely higher order.

The following is an example of a genuine higher order function, but
alas it is not very interesting (it is just an instance of
application): 

	\lambda: f:((N->N)->N)->N.f succ
	: ((N->N)->N)->N

--
Thorsten Altenkirch		LFCS, Edinburgh

"Germany still proves reluctant to exchange email with other countries 
efficiently" - Summer 1992 Systems Newsletter, Dep. of CS,Edinburgh

In article <ALTI.92Oct2123450@tanera.dcs.ed.ac.uk>, alti@dcs.ed.ac.uk (Thorsten Altenkirch) writes:
|> In article <1992Oct1.174259@cs.utwente.nl> ramaer@cs.utwente.nl (Mark Ramaer) writes:
|> 
|>    "alt" chooses between two "a"-parsers.
|> 
|>    > alt :: ([t]->Bool) -> Parser t r a -> Parser t r a -> Parser t r a
|>    > alt test aa bb = \contin input ->
|>    >       if test input
|>    >	then aa contin input
|>    >       else bb contin input
|> 
|>    > sequenceOption :: ([*]->bool) -> Parser t r a -> Parser t r [a]
|>    > sequenceOption test aa = alt test (sequence test aa) (empty [])
|> 
|>    "Parser t r a" is a 2nd order type, so "alt" and "sequenceOption"
|>    are 3rd order functions.
|> 
|> Thanks Mark, this certainly is a 3rd order function. In another
|> posting I tried to make the requirements more precise:
|> 
|>    If we have polymorphism, it is not clear what level to assign to type
|>    variables. In fact it is quite easy to get a 3rd order functions just
|>    by instantiating the type of polymorphic map by a 1st order function
|>    type for the input list. However, I am interested in *genuine* higher
|>    order functions, i.e. which do not show up as instantiations of
|>    polymorphic functions. This means that in this context I consider the
|>    order of a type variable as 0.
|> 
|> Your function alt can be obtained by instantiating a 2nd order
|> polymorphic function to the type Parser, right? In this way it is not
|> genuinely higher order.
|> 

Sorry, I have chosen a wrong example.  This function is from the same file:

cat >Try.lhs <<eoscript
> module Try(join) where

join :: (a -> b -> c) -> Parser t r a -> Parser t r b -> Parser t r c

> join semantic aa bb cont
>	= aa aCont
>	  where aCont a = bb (bCont a)
>		bCont a b = cont (semantic a b)
eoscript

Now hbc derives the type (note that my type specification is a comment):
join :: (a -> b -> c) -> ((a -> d) -> e) -> ((b -> f) -> d) -> (c -> f) -> e

(N.B. in the entire program d === e === f === [t]->r)

That should do,
Mark