Re: [Epigram] Re: Epigram and Mac OS X

Thorsten Altenkirch wrote: Another one for the implementors mtg? Certainly. Soon! I propose Nottingham/Beeston as a venue. We could have the offical part on the campus and the inoffical part in the Victorial Hotel in Beeston. I am happy to organize the official part. Sounds reasonable...

Re: [Epigram] new bug

Hi Thorsten Thorsten Altenkirch wrote: I jsut discovered a new bug, which seems to be related to the recent changes. I tried using the new facility, of being able to interactively use implicit parameters. However, the assignment between visible names and Horace 's names seems to be getting out

Re: [Epigram] Re: Epigram and Mac OS X

Thorsten Altenkirch wrote: Proposal: Friday 3 December for a workers hackshop. Can we bifuracate on this? :-) T. Well volunteered! I'll see how much incomprehensible code I can not document between now and then... Cheers Conor -- http://www.cs.rhul.ac.uk/~conor

[Epigram] Not the with rule; just an also ran

Hello all I don't use Epigram very often, but I like to have a bit of fun now and then. I thought I'd start with something pointless, a unit type... - data (-! where (---! ! Run : * )! run : Run )

Re: [Epigram] program inference, proper?

Edwin Brady wrote: On Tue, Jan 25, 2005 at 05:49:10PM +0100, Sebastian Hanowski wrote: Why can't Epigram give me something like this for a case on l (manipulated): ( l : List Nat ! let !--! !

[Epigram] Re: a case for star

Sebastian Hanowski wrote: * Thorsten Altenkirch [2005-01-25 18:30]: I see, you want iterated case analysis automatically. As Edwin points out, that's not always what you want. Maybe there should be a special gadget, case*, which iterates case analysis. I'm in favor. Let's call it 'staircase

Re: [Epigram] a naught E, non-structural call

Hi Sebastian Sebastian Hanowski wrote: ( f : Fin (suc m) - Fin (suc n) ! let !---! ! restrict _m _n f : Fin m - Fin n ) Should you be able to write a function with this type? I can certainly write a function from Fin 2 to Fin 1, but I shouldn't

Re: [Epigram] epigram tells me fibs

Yong Luo wrote: Primitive recursion + function types give you all functions provable total in Arithmetic, Goedel proved this (that's where System T comes from). Hello, Thorsten, In practice, it is sometimes not easy to change a non-primitive recursion to a primitive one. Here is

Re: [Epigram] why not replace failure with a context access?

Sebastian Hanowski wrote: Maybe it's just Epigram running out of RAM on my machine. But since freeing the program shed by shed was so easy i got nervous in the all-at-once case. Ah, that old thing... from the programmer. Moreover, an improved language design would

[Epigram] Re: Level n declaration

wrote: Dear Mr. Conor McBride, you have suggested the notion of a level parameter for declarations. E.g.: Level n data nat = zero | succ nat How should this be used? Has nat the type 'forall n:nat, Type n' (in Coq notation)? Can we apply nat only to constants or to arbitrary nats? The key

[Epigram] Re: [epigram-help] Status of type equality inference in Epigram?

Hi Adam Sorry to take so long. I've been on the move; I'm on the move again tomorrow. Keeping up with email is difficult. I hope you don't mind that I'm copying this reply to the Epigram mailing list: I expect some other people may be interested in the issues involved. Adam Chlipala wrote:

[Epigram] On Berry's Majority Function

Fit 2: On Berry's Majority Function Just to remind you all, I'm talking about maj :: Bool - Bool - Bool - Bool majTrueTrueTrue = True -- 1 majx TrueFalse = x -- 2 majFalse y True = y -- 3 majTrueFalse z = z -- 4 maj

Re: [Epigram] Partially defined functions and Pattern matching

Hello Yong Luo wrote: It is an undecidable problem in general whether patterns cover all the objects of a type. This is true but irrelevant. It is easy to construct a language of patterns which represent /evidence/ of covering, and for which checking is decidable. Semantically, the

Re: [Epigram] Partially defined functions and Pattern matching

Hi Yong Luo wrote: I think the problem is still about pattern coverage. It becomes clearer that pattern matching is different from case-spliting, and that is why the majority function comes into our discussion. As I have explained, functions such as the majority function present no more

[Epigram] Epigram 1 for 6.5

Hi folks By way of not falling too far behind the times, I've performed at least part of the necessary tweaks required to get Epigram 1 to build under ghc 6.5. This amounts to getting rid of the defunct IOExts stuff and wading through a bit of overlapping instance jiggery pokery. Remarks (1)

Re: [Epigram] Definitional equality in observational type theory

Hi Thorsten I'm not sure I understand what's going on here. Thorsten Altenkirch wrote: Indeed, in the setoid model we can construct a function f : A - [B] -- lift f : [A - B] if the setoid A is trivial, i.e. has the identity as its equivalence relation. I can

Re: [Epigram] Observational type theory

Hi Robin Robin Green wrote: Hi Thorsten, Thanks very much for your explanation - that was very helpful. Here is what I have written so far about OTT for my MRes literature review; please let me know if you see anything wrong. As I'm new to this, there probably is. A couple of small

[Epigram] Re: [epigram-help] implicit arguments

Hi I hope you don't mind me copying this reply to the mailing list, as it may be of more general interest. Jonathan Lee wrote: I've been trying the tutorial and I'm coming to the part about the (vec x) function. I'm a bit confused on how the implicit syntax as when I input: ( n : Nat ;

[Epigram] Re: [epigram-help] implicit arguments

Conor McBride wrote: I also apologise for the way Mozilla Thunderbird arbitrarily turns my code into jigsaw puzzles. I hate computers. All the best Conor

Re: [Epigram] How to define init for vectors?

Hi Serguey And here I got stuck: -- ( X : * ; xs : Vec (succ n) X ! let !--! ! vecInit xs : Vec n X ) vecInit xs = case xs { vecInit (vcons n' ns) = vcons

Re: [Epigram] Transpose again

Hi Mea culpa, I suspect. I haven't checked, but it looks like you've run into one of the known bugs. It's annoying, but there's a workaround. The trouble is the dog that doesn't bark... On 29 Feb 2008, at 14:16, Serguey Zefirov wrote: I decided to write transpose with implicit parameters. And

[Epigram] Fwd: JFP Special Issue on Generic Programming

Comrades Dr Hinze of Oxford requests that I pass on these joyous tidings to my nearest and dearest. I do so with pleasure. Cheers Conor Begin forwarded message: From: Ralf Hinze ralf.hi...@comlab.ox.ac.uk Date: 7 April 2009 08:18:28 BST To: Conor McBride co...@strictlypositive.org Subject