它在标题中说的是什么.如果我写一个类型签名,是否可以通过算法生成具有该类型签名的表达式？
似乎有可能做到这一点.我们已经知道,如果类型是库函数类型签名的特例,Hoogle可以通过算法找到该函数.另一方面,与一般表达式相关的许多简单问题实际上是无法解决的(例如,不可能知道两个函数是否做同样的事情),因此这是其中之一几乎难以置信.
一次问几个问题可能是不好的形式,但我想知道:
可以吗？
如果是这样,怎么样？
如果没有,是否有可能的限制情况？
两个不同的表达式很可能具有相同的类型签名.你能算出所有这些吗？甚至其中一些？
有没有人有工作代码,这是真的吗？
ehi*_*ird 34
Djinn为Haskell类型的受限子集执行此操作,对应于一阶逻辑.但它无法管理需要递归实现的递归类型或类型; 所以,例如,它不能写一个类型的术语(a -> a) -> a(类型fix),它对应于命题"如果a暗示a,那么a ",这显然是假的; 你可以用它来证明什么.实际上,这就是为什么fix会产生⊥.
如果你不容许fix,然后编写一个程序来给任何类型的术语是微不足道的; 该程序只需打印fix id每种类型.
Djinn主要是一个玩具,但它可以做一些有趣的事情,比如推导出正确的Monad实例Reader并Cont给出类型return和(>>=).您可以通过安装djinn软件包或使用lambdabot来尝试它,lambdabot将它集成为@djinn命令.
huo*_*uon 14
奥列格在okmij.org有这样的一个实现.这里有一个简短的介绍,但有文化的Haskell源包含过程的详细信息和描述.(我不确定这与Djinn的权力如何对应,但它是另一个例子.)
有些情况下没有独特的功能:
fst', snd' :: (a, a) -> a
fst' (a,_) = a
snd' (_,b) = b
不仅如此; 有些情况下有无数的功能:
list0, list1, list2 :: [a] -> a
list0 l = l !! 0
list1 l = l !! 1
list2 l = l !! 2
-- etc.
-- Or
mkList0, mkList1, mkList2 :: a -> [a]
mkList0 _ = []
mkList1 a = [a]
mkList2 a = [a,a]
-- etc.
(如果你只想要总的功能,然后再考虑[a]为受限于无限名单list0,list1等等,即data List a = Cons a (List a))
实际上,如果你有递归类型,任何涉及这些类型的类型都对应于无数个函数.但是,至少在上面的例子中,有相当数量的函数,因此可以创建一个包含所有函数的(无限)列表.但是,我认为类型[a] -> [a]对应于无数个无限数量的函数(再次限制[a]为无限列表),因此您甚至无法枚举所有函数!
(摘要:有些类型对应于有限的,可数无限且无数无限的函数.)
这通常是不可能的(对于像Haskell这样甚至没有强规范化属性的语言),并且只能在某些(非常)特殊情况下(对于更受限制的语言),例如当一个codomain类型只有一个时构造函数(例如,f :: forall a. a -> ()可以唯一地确定函数).为了将给定签名的一组可能定义减少到仅具有一个定义的单例集需要给出更多限制(例如,以附加属性的形式,仍然很难想象如果没有给出它将如何有用一个使用的例子).
从(n-)分类的观点来看,类型对应于对象,术语对应于箭头(构造函数也对应于箭头),并且函数定义对应于2个箭头.这个问题类似于是否可以通过仅指定一组对象来构造具有所需属性的2类别的问题.这是不可能的,因为你需要一个明确的箭头和两个箭头构造(即编写术语和定义),或演绎系统,它允许使用一组特定的属性(仍然需要明确定义)推导出必要的结构.
还有一个有趣的问题:给定ADT(即Hask的子类别)是否可以自动派生Typeable,Data(是的,使用SYB),Traversable,Foldable,Functor,Pointed,Applicative,Monad等实例(？ ).在这种情况下,我们有必要的签名以及其他属性(例如,monad定律,尽管这些属性不能在Haskell中表达,但它们可以用依赖类型的语言表示).有一些有趣的结构:
http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell
这显示了可以为列表ADT做什么.