我写了一小部分Haskell来弄清楚GHC如何证明对于自然数,你只能将偶数的一半:
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-}
module Nat where
data Nat = Z | S Nat
data Parity = Even | Odd
type family Flip (x :: Parity) :: Parity where
Flip Even = Odd
Flip Odd = Even
data ParNat :: Parity -> * where
PZ :: ParNat Even
PS :: (x ~ Flip y, y ~ Flip x) => ParNat x -> ParNat (Flip x)
halve :: ParNat Even -> Nat
halve PZ = Z
halve …我最近学到了一些关于F-algebras的知识:https: //www.fpcomplete.com/user/bartosz/understanding-algebras.我想将此功能提升到更高级的类型(索引和更高级别).此外,我检查了"给Haskell一个促销"(http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf),这非常有用,因为它给我自己的模糊命名"发明".
但是,我似乎无法创建适用于所有形状的统一方法.
代数需要一些"载体类型",但我们遍历的结构需要一定的形状(本身,递归应用),所以我想出了一个"Dummy"容器,可以携带任何类型,但形状符合预期.然后我使用一个类型系列来耦合它们.
这种方法似乎有效,导致我的'cata'功能的相当通用的签名.
但是,我使用的其他东西(Mu,Algebra)仍然需要为每个形状分别设置版本,只是为了传递一堆类型变量.我希望像PolyKinds这样的东西可以提供帮助(我成功地使用它来塑造虚拟类型),但它似乎只是意味着相反的方式.
由于IFunctor1和IFunctor2没有额外的变量,我试图通过附加(通过类型族)索引保留函数类型来统一它们,但由于存在量化,这似乎是不允许的,所以我留下了多个版本太.
有没有办法统一这两个案例？我是否忽略了一些技巧,或者这只是现在的限制？还有其他可以简化的事情吗？
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Cata where
-- 'Fix' for indexed types (1 index)
newtype Mu1 f a = Roll1 { unRoll1 :: f (Mu1 f) a }
deriving instance Show (f (Mu1 f) a) …我遇到了一个问题，迫使我将一个好的内衬分割成{}带中间层的块let。我根本不清楚这个原因。在这个最小的示例中，我能够找出问题所在：
struct AB {
a: u8,
b: u8,
}
impl AB {
fn foo(&self) -> String {
String::from("foo")
}
fn bar(self, x: String) -> String {
format!("{} - {} - {}!", x, self.a, self.b)
}
}
fn main() {
let x = AB { a: 3, b: 5 };
let result = x.bar(x.foo());
println!("{}", result);
}
我的印象是该bar函数的参数将在调用之前进行评估bar。在执行期间foo借入x，但在返回时String借用完成，因为String这不是参考轴承x的寿命。当bar …