Relax requirements for "deriving Nat(s)"

[GoogleCodeExporter]

What steps will reproduce the problem?
1.
Consider:
<http://code.google.com/p/omega/source/browse/trunk/work/LabelExpsWithTerminatio
nWitne
sses.prg?spec=svn215&r=215#11>
2.
The "deriving Nat(s)" syntax is not feasible here for two reasons:
a) there are three constructors
b) N and V both are unary
3.
This issue is about relaxing both:
"deriving Nat(V, N, s)" would signify
that
N . N . N . V  ==abbreviates==> 3s
(N . N . N . V) `lab  ==abbreviates==> 3s `lab

In short, allow non-nullary constructors as the "Zero".

Also, only V and N would participate in the Ns syntax.

But we can go further:
N Inf ==abbreviates==> (1+Inf)s
however I do not expect wonders...

Original issue reported on code.google.com by ggr...@gmail.com on 3 Jul 2009 at 10:29

[GoogleCodeExporter]

Implementation could be easier than it appears, because the pretty printer 
already displays composition:

prompt> N . N . N . V
<primfun (. <primfun (. <primfun (. <primfun N> <primfun N>)> <primfun N>)> 
<primfun V>)> : forall 
('a:Tag:*1).Label 'a -> Stage' (N (N (N (V 'a))))

Original comment by ggr...@gmail.com on 3 Jul 2009 at 10:42

[GoogleCodeExporter]

I have just watched the Eugene Summerschool videos, and Tim himself mentions in 
part 3 that
http://code.google.com/p/omega/source/browse/trunk/tests/Progress.prg#64
is basically a Nat-like definition with an extra constructor.

Original comment by ggr...@gmail.com on 31 Oct 2009 at 10:40

[GoogleCodeExporter]

see r334, could be a perfect match :-)

Original comment by ggr...@gmail.com on 26 Mar 2010 at 10:04

• Changed state: Started

[GoogleCodeExporter]

I want Tsil !
Snoc-lists!
These arise naturally, an application (a b c) is left associative (i.e. a 
snoc-list) whereas the type of a is (. -> (. -> 
(. -> .), i.e. a regular list.

Original comment by ggr...@gmail.com on 26 Mar 2010 at 10:09

[GoogleCodeExporter]

LeftLists are now supported :-)

Original comment by ggr...@gmail.com on 8 Dec 2010 at 3:28

[GoogleCodeExporter]

Here is the code that assembles the <primfun (. <fn> <fn>)> text:

$ svn blame LangEval.hs | grep nam2
     3     sheard   where h (Vlit (Symbol s1)) (Vlit (Symbol s2)) = return(Vprimfun (nam2 "swap" s1 s2) (downSwap [(s1,s2)] return))
     3     sheard nam2 string v1 v2 = "(" ++ string ++ " " ++ show v1 ++ " " ++ show v2 ++ ")"
     3     sheard                where h v2 = applyV (nam2 "$" v1 v2) v1 v2
     3     sheard           where h v2 = return(Vprimfun (nam2 "." v1 v2) g)

So all is needed to make this an Either SynExtCompositionTree String
Where constructors with "Raise"-like syn-ext would build a 
SynExtCompositionTree and composition would track these when they belong to the 
same syn-ext.

SMOP

Original comment by ggr...@gmail.com on 9 Dec 2010 at 12:01