[Haskell-cafe] Reflective capabilities of Haskell (cont'd)

Martin Hofmann martin.hofmann at uni-bamberg.de
Tue Mar 11 07:17:39 EDT 2008


I am trying to port a programme written in Maude, which is a reflective
language based on rewriting logic ( http://maude.cs.uiuc.edu/ ), to
Haskell. I thought using Template Haskell might be a good idea, but I
got stuck and now I am wondering if this is really possible in Haskell.
Let me give an example of a Maude module defining the function last over
a list of Peano numbers. 

        fmod LAST is
                sorts Peano PeanoList .
                
                op 0 : -> Peano [ctor] .
                op s : Peano -> Peano [ctor] .
                
                op [] : -> PeanoList [ctor] .
                op cons : Peano PeanoList -> PeanoList [ctor] .
                
                op last : PeanoList -> Peano .
                
                vars X Y : Peano .
                var Xs : PeanoList .
                
                eq last(cons(X,[])) = X .
                eq last(cons(X,cons(Y,Xs))) = last(cons(Y,Xs)) .
                
        endfm

So, last(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[])))) would reduce to
s(s(s(0))). The cool thing about Maude is, that terms, modules, ... can
be lifted to the meta level. For example:

        upModule('LAST, false)

would yield

        fmod 'LAST is
          including 'BOOL .
          sorts 'Peano ; 'PeanoList .
          none
          op '0 : nil -> 'Peano [ctor] .
          op '`[`] : nil -> 'PeanoList [ctor] .
          op 'cons : 'Peano 'PeanoList -> 'PeanoList [ctor] .
          op 'last : 'PeanoList -> 'Peano [none] .
          op 's : 'Peano -> 'Peano [ctor] .
          none
          eq 'last['cons['X:Peano,'`[`].PeanoList]] = 'X:Peano [none] .
          eq 'last['cons['X:Peano,'cons['Y:Peano,'Xs:PeanoList]]] =
last['cons[ 'Y:Peano,'Xs:PeanoList]] [none] .
        endfm
        
I also have access, e.g. to the defined type constructors.

So
        upOpDecls('LAST,false).
        
yields

        op '0 : nil -> 'Peano [ctor] .
        op '`[`] : nil -> 'PeanoList [ctor] .
        op 'cons : 'Peano 'PeanoList -> 'PeanoList [ctor] .
        op 'last : 'PeanoList -> 'Peano [none] .
        op 's : 'Peano -> 'Peano [ctor] .
        
Given an arbitrary function, I have access to its definition, its types
and the type constructors, all as ADTs.

Is this possible with Template Haskell, or in some other way?

Thanks a lot,

Martin









More information about the Haskell-Cafe mailing list