Applicative or monadic list forms?

[mstewartgallus]

Do we have applicative or monadic concatenation of list forms ? The current list form support mostly only seems to do mapping. I don't actually want to impose. Mostly I just want a confirmation I'm not missing something in the documentation.

I've found Ott very useful in formalizing my little logic programming language anyhow and I've wanted to drop by and thank the creators anyway.

Anyhow here's the problem case I've run into.

I have a little logic programming language and I made an original semantics in terms of which values satisfy a predicate (in a given environment.) See here.

However, after thinking about the issue I want to make a more explicit semantics of judgements stating precisely which "contexts" (relations) map to what lists of environments and matching terms.

If the previous approach was a little like the procedure denote then the new approach ought to be much more like search. We have explicit big step rules evaluating "contexts" into lists of normalized "terms" (values) that they match.

The prototype Ott code for the new approach is:

defns

sat :: '' ::=

defn
|- { N1 ; .. ; Nn } : t ::   :: v :: 'v_'
by

------------ :: tt
|- { tt } : unit

|- { N1 ; .. ; Nm } : t
|- { N'1 ; .. ; N'n } : t'
---------------------------------------- :: fanout
|- { Nm, N'n } : t * t'

% possible workaround?

|- { N1 ; .. ; Nm } : t
|- { N'1 ; .. ; N'n } : t
------------------------------------- :: merge
|- { N1 ; .. ; Nm ; N'1 ; .. ; N'n } : t

defn
E ! { D1 |- N1 ; .. ; Dn |- Nn } ::   :: sat :: 'sat_'
by

% possible workaround?

E ! { D1 |- N1 ; .. ; Dm |- Nm }
E ! { D'1 |- N'1 ; .. ; D'n |- N'n }
------------------------------------- :: merge
E ! { D1 |- N1 ; .. ; Dm |- Nm ; D'1 |- N'1 ; .. ; D'n |- N'n } 


--------------------- :: var
x ! { empty, x[N] |- N }

----------------- :: tt
tt ! { empty |- tt }

E ! { D1 |- tt ; .. ; Dm |- tt }
E' ! { D'1 |- N1 ; .. ; D'n |- Nn }
------------------------------------- :: step
(E,, E') ! { Dm ++ D'n |- Nn }

E ! { D1 |- N1 ; .. ; Dm |- Nm }
E' ! { D'1 |- N'1 ; .. ; D'n |- N'n }
------------------------------------------ :: fanout
(E, E') ! { Dm ++ D'n |- Nm, N'n }

E ! { D1 |- N1, N'1 ; .. ; Dm |- Nm, N'm }
E' ! { D'1, x[Nm], y[N'm] |- N''1 ; .. ; D'n, x[Nm], y[N'm] |- N''n }
----------------------------------------------------- :: let
(let (x, y) := E in E') ! { Dm ++ D'n |- N''n }

|- { N1 ; .. ; Nm } : t
E ! { D1, x[Nm] |- N'1 ; .. ; Dn, x[Nm] |- N'n }
---------------------------------------- :: abs
(lam x: t. E) ! { Dn |- Nm, N'n }

E ! { D1 |- N1, N'1 ; .. ; Dm |- Nm, N'm }
E' ! { D'1 |- Nm ; .. ; D'n |- Nm }
--------------------------------------- :: app
(E E') ! { Dm ++ D'n |- N'm }

At first I thought list forms might work for my approach but it seems list comprehensions don't really work for joining over multiple sets of values. I came up with a little workaround of the merge rule but it's not so great for a variety of reasons.

I think what I would really like is some form of notation like </ Di ++ D'j |- Ni, N'j // i, j /> that gives me every possible combination here kind of like how applicative functors or monads work. But I'm not really sure of the fully scope of the problem.

Anyway thanks. I've already found Ott very useful for prototyping even if you can always add new features.