headers
Sebastian Hanowski | 3 Apr 2007 10:57
Picon

if it's now or never, the delay monad will tell you later

Hello Josh Burdick,

* Am 29.03.07 schrieb Josh Burdick:
>   I have a question about an idea for adding "almost" a fixpoint to
> an otherwise strongly-normalizing language.  I'm going to write CC here
> to mean the Calculus of Constructions (without inductive types), but I
> think the idea is relevant to Epigram, since it's strongly normalizing.
> 
>   CC relies on strong normalization for its soundness, so you
> can't just toss an axiom like
> 
> fix : forall T. (T -> T) -> T

The epigram programming  language not only eschews  general recursion to
keep the logic of  the type system sound. It was  a /design decision/ by
McBride/McKinna

        http://foundations.cs.ru.nl/chitchat/slides/chit-swierstra.pdf

to default to  structural recursion since the novel  kind of interaction
the epigram  system provides  during program  development relies  on the
decidability  of the  type checking  relation. Which  get's lost  if you
allow  possibly non-terminating  computations in  types, as  for example
Lennart Augustsson's cayenne language did.

Conor  McBride   usually  suggests  to   have  fix  as  an   axiom  sans
computational  behaviour  during type  checking  to  answer demands  for
general recursion.

        http://www.haskell.org/pipermail/haskell/2004-August/014405.html
(Continue reading)

Permalink | Reply | 6 comments |
headers
Isaac Dupree | 3 Apr 2007 12:31
Favicon

Re: if it's now or never, the delay monad will tell you later


Sebastian Hanowski wrote:
>> It's sort of funny-looking, though: to write a factorial function,
>> for instance, you have to give "inf" an int, which doesn't get used
>> for anything.
> 
> To see how to write the factorial with the partial monad have a look at:
> 
>         http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=3

We don't really want factorial to be partial...

Anyway, neat seeing that, it makes it obvious how to write what I was
thinking of that two partial things can be combined such that you could
get either one... It's MonadPlus!

instance MonadPlus D where
 mzero = never
 mplus (Now a) _ = Now a
 mplus _ (Now a) = Now a
 mplus (Later d1) (Later d2) = mplus d1 d2

Although, this can pick an arbitrary answer based on the number of
cycles of recursion for each. What I was initially thinking was just for
functions like (&&).  In Haskell they're asymmetric, strict in the first
argument, where if it's False the whole function is false.  What would
be nice is a combinator that says that if partial argument A is foo, OR
partial argument B is bar, the whole function's answer is quux, no
matter if the other partial argument was _|_.
(Continue reading)

Permalink | Reply | 4 comments |
headers
Sebastian Hanowski | 3 Apr 2007 16:57
Picon

Re: if it's now or never, the delay monad will tell you later

* Am 03.04.07 schrieb Isaac Dupree:
> 
> Sebastian Hanowski wrote:
> > 
> > To see how to write the factorial with the partial monad have a look at:
> > 
> >         http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=3
> 
> We don't really want factorial to be partial...
> 
> Anyway, neat seeing that, it makes it obvious how to write what I was
> thinking of that two partial things can be combined such that you could
> get either one... It's MonadPlus!
> 
> instance MonadPlus D where
>  mzero = never
>  mplus (Now a) _ = Now a
>  mplus _ (Now a) = Now a
>  mplus (Later d1) (Later d2) = mplus d1 d2

Note that you have to record the depth of the recursion

        mplus (Later d1) (Later d2) = Later (mplus d1 d2)

or else you won't have

        mplus never never =~ never

and hence loose associativity.
(Continue reading)

Permalink | Reply | 3 comments |
headers
Isaac Dupree | 3 Apr 2007 22:04
Favicon

Re: if it's now or never, the delay monad will tell you later


Sebastian Hanowski wrote:
>> instance MonadPlus D where
>>  mzero = never
>>  mplus (Now a) _ = Now a
>>  mplus _ (Now a) = Now a
>>  mplus (Later d1) (Later d2) = mplus d1 d2
> 
> Note that you have to record the depth of the recursion
> 
>         mplus (Later d1) (Later d2) = Later (mplus d1 d2)
> 
> or else you won't have
> 
>         mplus never never =~ never
> 
> and hence loose associativity.

(mplus never never) _should_ be (never), right?

A different sort of implementation could run the two computations in
parallel, threads-style, and return whichever one finished first.
(subject to having a slightly different semantics - see my next comment)

> 
>> Although, this can pick an arbitrary answer based on the number of
>> cycles of recursion for each. What I was initially thinking was just for
>> functions like (&&).  In Haskell they're asymmetric, strict in the first
>> argument, where if it's False the whole function is false.  What would
>> be nice is a combinator that says that if partial argument A is foo, OR
(Continue reading)

Permalink | Reply | 2 comments |
headers
Sebastian Hanowski | 4 Apr 2007 01:00
Picon

Re: if it's now or never, the delay monad will tell you later

* Am 03.04.07 schrieb Isaac Dupree:
> 
> Sebastian Hanowski wrote:
> > 
> >        False && undefined --> False 
> >        True || undefined  --> True      
> > 
> > but
> > 
> >         liftM2 (&&) (Now False) never ~= never
> >         liftM2 (||) (Now True) never ~= never
> 
> As you show, they keep their short circuiting behavior - as well as
> gaining symmetric short-circuiting behavior such that (flip (&&)) =
> (&&), for example...?  How do they "seem to" lose their short circuiting
> behavior?-- I think at least one of us isn't understanding the other one
> yet.

I wanted to  point out that the pure boolean  functions don't care about
their second  arguments in the  given cases whereas the  lifted versions
do.

> > Seems that the delay monad is not an applicative functor.
> 
> Aren't ALL monads applicative functors? (though not the converse), with:
> pure = return
> (<*>) = ap

Of course you're right.  The behaviour of the lifted &&  and || is even
better  described  with applicative  functors  because  it's typical
(Continue reading)

Permalink | Reply | 0 comments |
headers
Josh Burdick | 11 Apr 2007 17:52

Re: if it's now or never, the delay monad will tell you later

On Tue, 2007-04-03 at 10:57 +0200, Sebastian Hanowski wrote:
> Hello Josh Burdick,

[...]

> The epigram programming  language not only eschews  general recursion to
> keep the logic of  the type system sound. It was  a /design decision/ by
> McBride/McKinna
> 
>         http://foundations.cs.ru.nl/chitchat/slides/chit-swierstra.pdf
> 
> to default to  structural recursion since the novel  kind of interaction
> the epigram  system provides  during program  development relies  on the
> decidability  of the  type checking  relation. Which  get's lost  if you

  That kind of interaction seems useful to me.

  And it does seem like _many_ useful programs can be written without
general recursion.  (SQL, or at least the subset of it based on the
relational calculus, disallows nonterminating queries.  But it's still
pretty popular, probably partly because this makes some query rewriting
easier.)

  The main thing I was wondering if you'd need something like a fixpoint
for was to write a type-checker or OTT interpreter in OTT.  Do you?  The
Coq-in-Coq paper points out that because of Godel's incompleteness
theorem, you can't write a proof-checker, or indeed an interpreter, for
Coq in Coq.

  I assume the same restriction applies to OTT.  Being able to write an
(Continue reading)

Permalink | Reply | 0 comments |
headers
Isaac Dupree | 15 Apr 2007 00:55
Favicon

background reading - _Type Theory and Functional Programming_?


I've started reading the 1991 book _Type Theory and Functional
Programming_ (online at http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
, found through http://haskell.org/haskellwiki/Books )... from its
introductory material it seems like it will be useful background
material for understanding various ideas in this area ((pre-)epigram).
Of course, as it admits, it can't keep up with the following (16) years'
active research by staying the same text :).  But I was wondering
whether it would be worth putting on the "Background Reading" part of
the website that is presently empty.  Does anyone know this book?  If I
get through a significant part of it, I'll report how it was for me anyway.

Isaac
Permalink | Reply | 1 comment |
headers
Wouter Swierstra | 15 Apr 2007 11:58
Picon

Re: background reading - _Type Theory and Functional Programming_?

Hi Isaac,

I've read (parts of) the book as well. I'm not too fond of it. It is  
probably one of the only books that explains type theory for  
functional programmers - which is great of course. Unfortunately, I  
read through most of it and could not shake the feeling that I wasn't  
really learning anything. It somehow doesn't always convey the "joy  
of type theory" (well, for my personal taste at least).

Other background reading you might be interested in include:

Programming in Martin-Lofs Type Theory. Available from:
http://www.cs.chalmers.se/Cs/Research/Logic/book/

http://www.amazon.co.uk/Lectures-Curry-Howard-Isomorphism-Foundations- 
Mathematics/dp/0444520775/ref=sr_1_2/026-1815313-5521242? 
ie=UTF8&s=books&qid=1176630898&sr=8-2
Lecture notes on the Curry-Howard Isomorphism.
A bit technical, but contains just about everything you'll ever need  
to know.

I also found it instructive to familiarize myself with other proof  
assistants based on dependent types. You might want to look into Coq,  
for instance. It's a very mature and well-documented system. The  
Coq'Art book is a great place to start.

Hope these comments help,

  Wouter
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jacques Carette | 25 Apr 2007 16:01
Picon
Picon
Favicon

Programming Languages and Mechanised Mathematics -- deadline extension

[Extended deadline: submissions now due May 2nd, 2007]

Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>
Hagenbergs, Austria
June 29-30, 2007.

The intent of this workshop is to examine more closely the intersection 
between
programming languages and mechanized mathematics systems (MMS). By MMS, we
understand computer algebra systems (CAS), [automated] theorem provers
(TP/ATP), all heading towards the development of fully unified systems (the
MMS), sometimes also called universal mathematical assistant systems 
(MAS) (see
Calculemus 2007
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>).

There are various ways in which these two subjects of /programming 
languages/ and /systems for mathematics/ meet:

   * Many systems for mathematics contain a dedicated programming
     language. For instance, most computer algebra systems contain a
     dedicated language (and are frequently built in that same
     language); some proof assistants (like the Ltac language for Coq)
     also have an embedded programming language. Note that in many
     instances this language captures only algorithmic content, and
     /declarative/ or /representational/ issues are avoided.
   * The /mathematical languages/ of many systems for mathematics are
(Continue reading)

Permalink | Reply | 0 comments |

Gmane