小编nit*_*101的帖子

我正在使用portaudio处理一些音频.只要有要处理的音频数据,haskell FFI绑定就会调用用户定义的回调.应该非常快速地处理此回调,理想情况下不需要I/O. 我想保存音频输入并快速返回,因为我的应用程序不需要实时响应音频(现在我只是将音频数据保存到文件中;稍后我将构建一个简单的语音识别系统) .

我喜欢这个想法,pipes并认为我可以使用该库.问题是我不知道如何创建一个Producer返回通过回调传入的数据.

我该如何处理我的用例？

以下是我现在正在使用的内容,如果有帮助的话(基准mvar现在不能正常工作,但我不喜欢将所有数据存储在seq中...我宁愿处理它而不是它来代替刚刚结束):

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

module Main where

import Codec.Wav

import Sound.PortAudio
import Sound.PortAudio.Base
import Sound.PortAudio.Buffer

import Foreign.Ptr
import Foreign.ForeignPtr
import Foreign.C.Types
import Foreign.Storable

import qualified Data.StorableVector as SV
import qualified Data.StorableVector.Base as SVB

import Control.Exception.Base (evaluate)

import Data.Int
import Data.Sequence as Seq

import Control.Concurrent

instance Buffer SV.Vector a where
  fromForeignPtr fp = return . SVB.fromForeignPtr fp
  toForeignPtr = return . (\(a, b, c) -> (a, c)) . SVB.toForeignPtr …

我是Coq的新手,我正在努力证明一些非常基本的东西

引理eq_if_eq:forall a1 a2,(如果beq_nat a1 a2则a2否a1)= a1.

我努力通过下面发布的解决方案,但我认为必须有更好的方法.理想情况下,我希望beq_nat a1 a2在将案例值放入假设列表时干净利落.有没有一种策略t可以使用t (beq_nat a1 a2)两个子句,一个在哪里beq_nat a1 a2 = true,另一个在哪里beq_nat a1 a2 = false？显然,induction非常接近,但它失去了它的历史.

这是我努力的证明:

Proof.
Hint Resolve beq_nat_refl.
Hint Resolve beq_nat_eq.
Hint Resolve beq_nat_true.
Hint Resolve beq_nat_false.
intros.
compare (beq_nat a1 a2) true.
intros. assert (a1 = a2). auto. 
replace (beq_nat a1 a2) with true. auto.
intros. assert (a1 <> a2). apply beq_nat_false.
apply not_true_is_false. auto.
assert (beq_nat a1 a2 …

我为表达式创建了一个GADT.当我对具有约束的构造函数进行模式匹配时,类型检查器无法推断出对构造函数约束中使用的类型变量的约束.我认为代码和错误信息更具说明性.

{-# LANGUAGE GADTs, MultiParamTypeClasses #-}
import Data.Word

data Expr a where
  Value :: a -> Expr a
  Cast :: (Castable a b) => Expr a -> Expr b

class Castable a b where
  cast :: a -> b

instance Castable Word64 Word32 where
  cast = fromIntegral

instance (Show a) => Show (Expr a) where
  show (Cast e) = "Cast " ++ show e -- ERROR

我得到的错误:

gadt.hs:16:30:
    Could not deduce (Show a1) arising from a use of `show'
    from …

这就是我想要做的:

data X = I Int | D Double deriving (Show, Eq, Ord)

{-
-- A normal declaration which works fine
instance Num X where
  (I a) + (I b) = I $ a + b
  (D a) + (D b) = D $ a + b
  -- ...   
-}                                          

coerce :: Num a => X -> X -> (a -> a -> a) -> X
coerce (I a) (I b) op = I $ a `op` b
coerce (D …