headers
Conor McBride | 12 Nov 2004 10:50
Picon
Favicon

vector_bin_op2

Folks...

Is anyone else reading Coq-club just now?

Conor

--

-- 
http://www.cs.rhul.ac.uk/~conor
Permalink | Reply | 1 comment |
headers
Yong Luo | 12 Nov 2004 15:38
Picon
Picon

Re: vector_bin_op2

It will become much worse, for example, if one wants to define addition
of two matix. I don't think any mathematitian will accept that definition.

Yong

On Fri, 12 Nov 2004, Conor McBride wrote:

> Folks...
>
> Is anyone else reading Coq-club just now?
>
> Conor
>
> --
> http://www.cs.rhul.ac.uk/~conor
>
Permalink | Reply | 0 comments |
headers
Sebastian Hanowski | 16 Nov 2004 11:10
Picon

Escape from planet Xemacs

The crib2graphy of 

http://www.cs.rhul.ac.uk/~conor/notions/html.html

gives another good reason why

"..., the sooner we can escape from xemacs, the better."

since it shows quite painly how Epigram Programs could look just now if
only Xemacs would support UTF-8 character encoding, like any sensible
editor does.

Regards,
s~
Permalink | Reply | 10 comments |
headers
Sebastian Hanowski | 16 Nov 2004 11:09
Picon

Epitomes of Epigram Programming


"Please join and let us know what fun you do/don't have."

Can't decide whether i do or i don't. Here's (a quarter of) my do-Zen:

Epigram supports the MTV Jackass-kind-of-stunt-style-of-programming:
Everytime your code sticks its head out of a shed it gets tared and
feathered (with brown colour and question marks) by the elaborator.

---

A quasiquote from P. Wadler:
`(Calculating , <at> '(types) is better than , <at> '(type) scheming.)

---

Epigram vs. Tetris

Machine-generated patterns (there: a.k.a. tetrominos) state problems to
be solved interactively by closing gaps (here: in the source code),
which in turn sets the ground (sic!) for new solutions to new problems.

Cheers,
s~
Permalink | Reply | 0 comments |
headers
Jules Bean | 16 Nov 2004 15:58
Picon

Re: Escape from planet Xemacs


On 16 Nov 2004, at 10:10, Sebastian Hanowski wrote:

> The crib2graphy of
>
> http://www.cs.rhul.ac.uk/~conor/notions/html.html
>
> gives another good reason why
>
> "..., the sooner we can escape from xemacs, the better."
>
> since it shows quite painly how Epigram Programs could look just now if
> only Xemacs would support UTF-8 character encoding, like any sensible
> editor does.
>

As far as I can tell, xemacs does actually have enough unicode support  
for this, given appropriate fonts.

Which doesn't mean that I don't agree about escaping from xemacs,  
anyhow.

Refs:

http://www.tug.org/ftp/texlive/Contents/testinstalled/xemtex/doc/ 
xemacs/xemacs-faq.html

http://tats.haun.org/mule-ucs/
(Continue reading)

Permalink | Reply | 9 comments |
headers
Sebastian Hanowski | 16 Nov 2004 20:12
Picon

Re: Escape from planet Xemacs

* Jules Bean [2004-11-16 17:25]:
> As far as I can tell, xemacs does actually have enough unicode support
> for this, given appropriate fonts.

Maybe you're right, but isn't that through an extra lib? Anyway it seems
that i just didn't google hard enough. All i once got was patches to the
Xemacs sources. Since  we're dealing with people here  who "hate writing
editors", i considered this a no-opt.

s~
Permalink | Reply | 8 comments |
headers
Conor McBride | 17 Nov 2004 17:04
Picon
Favicon

Re: Escape from planet Xemacs

Sebastian Hanowski wrote:
> * Jules Bean [2004-11-16 17:25]:
> 
>>As far as I can tell, xemacs does actually have enough unicode support
>>for this, given appropriate fonts.
> 
> 
> Maybe you're right, but isn't that through an extra lib? Anyway it seems
> that i just didn't google hard enough. All i once got was patches to the
> Xemacs sources. Since  we're dealing with people here  who "hate writing
> editors", i considered this a no-opt.

I hate writing editors. Doesn't mean everyone who might work on the system
hates writing editors. Doesn't mean everyone who hates writing editors
won't do it anyway. Funnily enough, the thing I hate most about writing
editors is keeping all the metrics and markers in sync with the buffer
contents, which is something dependent types might give me more of a handle
on.

I am having a lot of (too much?) fun with unicode in my latest scribblings.
It does look better than boring old ascii. I'd like unicode symbols to be
an available choice.

However, the escape I'm looking for is the separation of the interface
from the elaborator. I'd like to make it possible (in principle) for more
than one interface to be hitched up to the system. If we can sort out the
API for querying and submitting code to the elaborator, then you can all
do whatever you like.

I'm working on it. Amongst other things.
(Continue reading)

Permalink | Reply | 7 comments |
headers
Sebastian Hanowski | 18 Nov 2004 10:43
Picon

Things amongst others (was: Re: Escape from planet Xemacs)

* Conor McBride [2004-11-17 18:38]:
> I hate  writing editors. Doesn't mean  everyone who might work  on the
> system hates writing editors. Doesn't  mean everyone who hates writing
> editors won't do it anyway.

In the end I wasn't aiming at what the Epigram gang ist capable of doing
or willing to do. I just thought dependencies for running Epigram should
be low,  which in my opinion  wouldn't be the case  if its prerequesites
included  the fetching  of  patches or  elisp-libraries  for Xemacs  and
re-/byte-compiling.

> Funnily enough, the thing I hate most about writing editors is keeping
> all the metrics and markers in sync with the buffer contents, which is
> something dependent types might give me more of a handle on.

So one day  we'll see the Epimacs?  By the way, as the  success of Emacs
shows editors are  best written in languages with  dynamic scoping. Make
shure Epigram has this feature.

> I  am having  a lot  of  (too much?)  fun  with unicode  in my  latest
> scribblings.  It does  look better  than  boring old  ascii. I'd  like
> unicode symbols to be an available choice.

Which implies using UTF-8 character  encoding, because that would retain
backward compatibility.

> However, the escape I'm looking for is the separation of the interface
> from the elaborator.  I'd like to make it possible  (in principle) for
> more than one interface to be hitched up to the system.
(Continue reading)

Permalink | Reply | 6 comments |
headers
Conor McBride | 18 Nov 2004 12:07
Picon
Favicon

Re: Things amongst others

Sebastian Hanowski wrote:
> * Conor McBride [2004-11-17 18:38]:
>>Funnily enough, the thing I hate most about writing editors is keeping
>>all the metrics and markers in sync with the buffer contents, which is
>>something dependent types might give me more of a handle on.
> 
> 
> So one day  we'll see the Epimacs?  By the way, as the  success of Emacs
> shows editors are  best written in languages with  dynamic scoping. Make
> shure Epigram has this feature.

Being an old lisper, I'm rather fond of dynamic scoping. Turns out you
can get quite a long way towards it in a statically scoped language with
implicit arguments. I mean, there's more than one way to infer an
argument. At the moment, when we have a thing of type

   all _x : S => T

we create a new metavariable x : S and hope it gets solved by unifying
T with something, but there are at least two other things one might do:

   (1) look for an obvious element of S lying around. Of course, if S
         is Bool then there is no obvious preferred choice, but if S is
         (So whatever), then you're either lucky or you're not. The
         sorting function given at

           http://www.cs.rhul.ac.uk/~conor/a-case/16so/index.html

         and so on, exploits this idea to make treesort-which-sorts look
         quite like ordinary treesort. The proofs you need are exactly
(Continue reading)

Permalink | Reply | 2 comments |
headers
Thorsten Altenkirch | 18 Nov 2004 12:12
Picon
Gravatar

Re: Things amongst others


> So one day  we'll see the Epimacs?  By the way, as the  success of Emacs
> shows editors are  best written in languages with  dynamic scoping. Make
> shure Epigram has this feature.

That's a bit of a short-cut conclusion.

Dynamic scoping achieves the right thing the wrong way. We shouldn't abuse variable binding
to model access models to a state. Indeed Epimacs should be written in Epigram, what else?

T.
--

-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham

This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
Permalink | Reply | 1 comment |

Gmane