我最近发现类型孔与样张上的图案匹配相结合,在Haskell中提供了非常好的Agda式体验.例如:
{-# LANGUAGE
DataKinds, PolyKinds, TypeFamilies,
UndecidableInstances, GADTs, TypeOperators #-}
data (==) :: k -> k -> * where
Refl :: x == x
sym :: a == b -> b == a
sym Refl = Refl
data Nat = Zero | Succ Nat
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
type family a + b where
Zero + b = b
Succ a + b = Succ …既阿格达和伊德里斯有效地禁止图案类型的值相匹配Type.似乎Agda总是在第一种情况下匹配,而Idris只是抛出一个错误.
那么,为什么typecase是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的更多信息.
我只能以相当笨拙的方式在Idris 0.9.12中执行rank-n类型:
tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)
我需要在有类型应用程序的地方使用下划线,因为当我尝试隐藏(嵌套)类型参数时,Idris会抛出解析错误:
tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile
一个可能更大的问题是我根本不能在更高级别的类型中进行类约束.我无法将以下Haskell函数转换为Idris:
appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x
这也防止我使用伊德里斯用作类型同义词类型,例如Lens,这是Lens s t a b = …
Coq 常见问题解答说功能扩展性与预测性一致Set.从这一点来看,我不完全清楚它是否与不可预测的一致Set(或者在这种情况下可能是一致性).
在Haskell(和Rust等)中,我可以拥有受其他实例约束的实例:
data Pair a b = Pair a b
instance (Eq a, Eq b) => Eq (Pair a b) where
Pair a b == Pair a' b' = a == a' && b == b'
使用Java接口我不能.我必须要求类型参数Pair始终实现Eq,否则我根本无法实现Eq<Pair<A, B>>:
interface Eq<A> {
public boolean eq(A other);
}
class Pair<A extends Eq<A>, B extends Eq<B>> implements Eq<Pair<A, B>> {
A a;
B b;
public boolean eq(Pair<A, B> other){
return a.eq(other.a) && b.eq(other.b);
}
}
我希望有类似的东西:
class Pair<A, …采取以下代码:
#include <type_traits>
#include <iostream>
template <class T>
void print(T &&t){
std::cout << t << std::endl;
}
template<class T, T val>
struct Foo{
static constexpr T value = val;
};
int main(){
print(Foo<int, 123>::value);
}
它拒绝在Clang 3.3和GCC 4.8.1下编译("undefined reference to Foo<int, 123>::value"),这让我感到困惑,因为Foo它完全相同std::integral_constant,并且相同的代码运行良好integral_constant.它也在打印功能中使用普通左值引用失败.有关此行为的任何解释？
这个极小的例子也出现了这个问题:
template<class T>
struct Bar{
static const bool value = true;
};
这个最近的SO问题促使我在Haskell中编写了一个不安全且纯粹的ST monad仿真,这是一个稍微修改过的版本,你可以在下面看到:
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-}
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.List
newtype ST s a = ST (State ([Any], Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show
newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
(env, i) <- get
put (unsafeCoerce a : env, i + 1)
pure (STRef i)
update :: [a] -> (a -> a) …我是一个Haskell新手,我想知道为什么没有替代实例,Either但是半群,其行为与我期望的替代:
instance Semigroup (Either a b) where
Left _ <> b = b
a <> _ = a
此实例丢弃或更正"错误",当两个操作数都被标记时Right,它将采用第一个.这不是替代品提供的"选择"吗？
我希望semigroup实例看起来大致如下:
instance (Semigroup b) => Semigroup (Either a b) where
Left e <> _ = Left e
_ <> Left e = Left e
Right x <> Right y = Right (x <> y)
这意味着它传播错误并附加常规结果.
我想我有一个错误的概念Either或涉及的类型类.
假设存在以下类型索引列表和复制函数:
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: a -> Vect n a -> Vect (n + 1) a
replicateVec :: forall n a. Sing n -> a -> Vect n a
(你可以replicateVec在这个问题中找到几个不同的实现).
我想创建replicateVecSigma一个Vect在依赖对中返回a 的函数.理想情况下,它将如下所示:
replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)
怎么Sigma用来写这个功能？如何写出函数的类型？
实际上,我能够实现replicateVecSigma如下,但它似乎不是很干净:
data Foo a b (m :: …Agda 2.3.2.1无法看到以下函数终止:
open import Data.Nat
open import Data.List
open import Relation.Nullary
merge : List ? ? List ? ? List ?
merge (x ? xs) (y ? ys) with x ?? y
... | yes p = x ? merge xs (y ? ys)
... | _ = y ? merge (x ? xs) ys
merge xs ys = xs ++ ys
Agda wiki说,如果递归调用的参数按字典顺序减少,那么终止检查器就可以了.基于此,似乎这个功能也应该通过.那我在这里错过了什么？此外,在以前版本的Agda中它可能还可以吗？我在互联网上看过类似的代码,没有人提到那里的终止问题.