什么语言有等式重写?

功能程序效率低下的一个典型例子是 reverse 根据规范编写的函数

import Prelude()

[] ++ ys = ys
(x:xs) ++ ys = x:(xs ++ ys)

reverse []     = []
reverse (x:xs) = (reverse xs) ++ [x]

利用结合性,我们可以得到一个有效的反向

-------- REWRITE ------

-- RULE : ++ relation (deduced)
-- reverse xs = reverse xs ++ []

-- RULE : [] relation -- case split
-- reverse []      = reverse [] ++ []
-- reverse (x::xs) = reverse (x::xs) ++ [] 

-- RULE : reverse relation 
-- reverse []      = []                
-- reverse (x::xs) = (reverse xs ++ [x]) ++ []

-- RULE : ++ relation (deduced)
-- reverse []      = []                
-- reverse (x::xs) = reverse xs ++ ([x] ++ [])

-- RULE : ++ relation
-- reverse []      = []                
-- reverse (x::xs) = reverse xs ++ (x::[])

-- RULE :  (language)
-- reverse' []      _   = []                
-- reverse' (x::xs) acc = reverse xs ++ acc
-- reverse  xs = reverse' xs []

reverse_eff xs = reverse' xs []
  where 
    reverse' [] ys  = ys
    reverse' (x:xs) ys  = reverse' xs (x:ys)

然而,问题首先来自哪里?

• 我们指示具体订购 ++
• 我们的语言定义的构图定义了我们语言的构图顺序 ++
• 我们的语言不了解法律,不了解源于代码本身的法律,也不知道效率的概念。

我们 真正地 我想做的是:

• 指定(功能)关系 ++ 根据其所有法律适当地进行商业化
• 对它使用关系组合,它隐藏了将使用的特定括号
• 在使用站点,选择一个最适合我们访问模式和目标的括号(在 颠倒 ,这意味着移动所有括号以匹配生成列表的方式)

有没有哪种语言能产生一些规律,并根据某种标准寻找最佳重写?