在Idris/Haskell中,可以通过注释类型和使用GADT构造函数来证明数据的属性,例如使用Vect,但是,这需要将属性硬编码到类型中(例如,Vect必须是与List不同的类型).是否可以使用具有开放属性集的类型(例如包含长度和运行平均值的列表),例如通过重载构造函数或使用效果的静脉？
看起来像Applicative,Monad和Arrow这样的类型类在类型类中有某种类型的等价类型,例如Alternative,MonadPlus和ArrowPlus.例如,Applicative和Alternative可用于定义以下内容:
(<&&>) :: Applicative f => f a -> f b -> f (a, b)
a <&&> b = (,) <$> a <*> b
(<||>) :: Alternative f => f a -> f b -> f (Either a b)
a <||> b = (Left <$> a) <|> (Right <$> b)
但是,在所有这些情况下(以及ArrowChoice),产品类型类是sum类型的先决条件.是否存在依赖于先决条件类的类型规则或常用函数？该Typeclassopedia触及了这些关系,但不幸的是我无法找到的依赖任何明确的理由.
通常为Arrows提供的大多数激励示例都显示了如何在Hask之上构建更复杂的计算系统(例如,Kleisli类别的效果,Arrowized FRP等)是否已经完成了使用Arrows编写较低级别的任何工作代码(例如汇编,Javascript)？虽然这可能不完全符合Arrow的标准定义(特别是arr :: (a -> b) -> cat a b),但似乎Arrows形成了某种连接编程的强大基础.