如何解决Idris中元组的智能构造函数
我开始阅读“使用Idris进行类型驱动的开发”的第6章,并尝试为元组向量编写智能构造函数。
TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) a = (a,TupleVect k a)
someValue : TupleVect 4 Nat
someValue = (1,2,3,4,())
TupleVectConstructorType : Nat -> Type -> Type
TupleVectConstructorType n typ = helper n
where
helper : Nat -> Type
helper Z = TupleVect n typ
helper (S k) = typ -> helper k
tupleVect : (n : Nat) -> (a : Type) -> TupleVectConstructorType n a
tupleVect Z a = ()
tupleVect (S Z) a = \val => (val,())
tupleVect (S (S Z)) a = \val2 => \val1 => (val2,val1,())
-- ??? how to create tupleVect (S k) a
如何为任意k创建构造函数?
解决方法
基本上是@Matthias Berndt的想法。倒数要添加的箭头,同时使最后一个元组更长。为此,我们需要从TupleVectType
访问更为宽松的帮助程序。
TupleVectType' : Nat -> Nat -> Type -> Type
TupleVectType' Z n a = TupleVect n a
TupleVectType' (S k) n a = a -> TupleVectType' k (S n) a
TupleVectType : Nat -> Type -> Type
TupleVectType n = TupleVectType' n Z
tupleVect : (n : Nat) -> (a : Type) -> TupleVectType n a
tupleVect n a = helper n Z a ()
where
helper : (k,n : Nat) -> (a : Type) -> (acc : TupleVect n a)
-> TupleVectType' k n a
helper Z n a acc = acc
helper (S k) n a acc = \x => helper k (S n) a (x,acc)
someValue2 : TupleVect 4 Nat
someValue2 = (tupleVect 4 Nat) 4 3 2 1
请注意,这将导致\v2 => \v1 => (v1,v2,())
而不是\v2 => \v1 => (v2,v1,())
,因为前者更适合TupleVect (S k) a = (a,TupleVect k a)
的递归定义。
我对Idris几乎一无所知,只是它是一种依赖类型的,类似于Haskell的语言。但是我发现这个问题很有趣,所以我试了一下。
很显然,您需要在此处递归解决方案。我的想法是使用一个附加参数f
来累积该函数到目前为止已消耗的val1
.. val_n
个参数。达到基本情况后,将返回f
。
tupleVectHelper Z a f = f
tupleVectHelper (S n) a f = \val => tupleVectHelper n a (val,f)
tupleVect n a = tupleVectHelper n a ()
我不知道这是否行得通,并且我还没有弄清楚如何编写tupleVectHelper
的类型,但是我尝试手动为n = 3
进行替换,并且看起来在纸上进行计算,尽管生成的元组向后。但是我认为应该不难解决。
希望这会有所帮助!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。