Maude-help mailing list

[Francisco Durán <narudocap AT gmail.com>]

Hi Raghu,

Many years ago we proposed a generic solution, as an extension of Full Maude. 
However, after so many years it has got completely outdated, and it would 
require a complete re-implementation.

Manuel Clavel, Francisco Durán, Narciso Martí-Oliet:
Polytypic Programming in Maude. WRLA 2000: 339-360
https://urldefense.com/v3/__https://doi.org/10.1016/S1571-0661(05)80135-5__;!!DZ3fjg!57mBBiriInbUeVq9cBptSLwjv51JvWKRtv-hI1gMGo93ICAuBMr8aPwni5RSpnnjZMPrVnJqUhxdDZ_3zSMN0SRdtX1MCQ$
 

I can see two ways to handle this kind of things: parameterization and 
metalevel. 

The simplest solution is using parameterization. E.g., 

fth FUN is
inc TRIV .
op f : Elt -> Elt .
endfth

view FUN from TRIV to FUN is
sort Elt to Elt .
endv 

fmod MAPF{X :: FUN} is
pr LIST{FUN}{X} .
op map : List{FUN}{X} -> List{FUN}{X} .
var X : X$Elt .
var L : List{FUN}{X} .
eq map(X L) = f(X) map(L) .
eq map(nil) = nil .
endfm

view inc from FUN to NAT is 
sort Elt to Nat .
var N : Elt .
op f(N) to term N + 1 .
endv

fmod MAPinc is
pr MAPF{inc} .
endfm

red map(2 3 4) .

In this solution the function is not a parameter of the map, it's provided in 
the view. 

Metaprogramming provides a simpler solution

fmod MAPinc is
pr META-LEVEL .
op map : Qid NatList -> NatList .
var F : Qid .
var X : Nat .
var L : NatList .
eq map(F, X L) = downTerm(getTerm(metaReduce(upModule('NAT, false), 
F[upTerm(X)])), 0) map(F, L) .
eq map(F, nil) = nil .
endfm

red map('s_, 2 3 4) .

Best regards, 

Francisco

Attachment: hop.maude
Description: Binary data

Attachment: hopml.maude
Description: Binary data

> On 2 Dec 2023, at 07:30, Raghu Ranganathan <rraghu.11502 AT gmail.com> wrote:
> 
> I would like to create an operator that can take in a different operator 
> and add that operator to its expansion. I want to implement things like map 
> and filter in haskell or find useful alternatives to those.
> 
> For example:
> 
> mod FUNC{X :: TRIV} is
>   ex LIST*{X} .
>   pr META-TERM . 
>   var F : Term .
>   var Y : List{X} .
>   var N : Nat .
>   op map : X List{X} -> List{X} .
>   op inc : Nat -> Nat .
>   
>   eq map(F, Y) = append( [F(head(Y))], map(F, tail(Y)) ) .
>   eq inc(X) = X + 1 .
> endm 
> 
> then red map(inc, [1 2 3])  should reduce to [2 3 4].
> 
> I'm not sure how to make this parse and work correctly. Thank you for your 
> help in advance.