小编Pet*_*lák的帖子

关于归纳数据类型和模式匹配的 Agda手册:

为确保正常化,归纳事件必须出现在严格的正位置.例如,不允许以下数据类型:

data Bad : Set where
  bad : (Bad ? Bad) ? Bad

Run Code Online (Sandbox Code Playgroud)

因为构造函数的参数中存在负面的Bad.

为什么归纳数据类型需要此要求？

举个例子,假设我想在列表上写一个monadic和非monadic地图.我将从monadic开始:

import Control.Monad
import Control.Monad.Identity

mapM' :: (Monad m) => (a -> m b) -> ([a] -> m [b])
mapM' _ [] = return []
mapM' f (x:xs) = liftM2 (:) (f x) (mapM f xs)

现在我想重用代码来编写纯map(而不是重复代码):

map' :: (a -> b) -> ([a] -> [b])
map' f = runIdentity . mapM' (Identity . f)

什么是必要的,使map'优化的,如果它被明确地写的map是？特别是:

1. 是否有必要写

   {-# SPECIALIZE mapM' :: (a -> Identity b) -> ([a] -> Identity [b]) #-} …

   Run Code Online (Sandbox Code Playgroud)

通常我需要向ADT添加字段,只记忆一些冗余信息.但我还没有完全弄清楚如何做得好而有效.

显示问题的最佳方法是举个例子.假设我们正在使用无类型的lambda术语:

type VSym = String

data Lambda = Var VSym 
            | App Lambda Lambda
            | Abs VSym Lambda

有时我们需要计算一个术语的自由变量集:

fv :: Lambda -> Set VSym
fv (Var v)    = Set.singleton v
fv (App s t)  = (fv s) `Set.union` (fv t)
fv (Abs v t)  = v `Set.delete` (fv t)

很快我们意识到重复计算fv是我们应用的瓶颈.我们想以某种方式将它添加到数据类型中.喜欢:

data Lambda1 = Var (Set VSym) VSym
             | App (Set VSym) Lambda Lambda
             | Abs (Set VSym) VSym Lambda

但它使定义相当丑陋.几乎(Set VSym)比其他所有人都占用更多的空间.而且,它在所有使用的函数中打破了模式匹配Lambda.更糟糕的是,如果我们后来决定添加一些其他的memoizing字段,我们将不得不再次重写所有模式.

如何设计一个通用的解决方案,允许轻松,不引人注意地添加这些记忆字段？ …

我创建了这个小程序,它创建了一个长时间运行的thunk,最终因异常而失败.然后,多个线程尝试评估它.

import Control.Monad
import Control.Concurrent
import Control.Concurrent.MVar

main = do
    let thunk = let p = product [1..10^4]
                 in if p `mod` 2 == 0 then error "exception"
                                      else ()
    children <- replicateM 2000 (myForkIO (print thunk))
    mapM_ takeMVar children

-- | Spawn a thread and return a MVar which can be used to wait for it.
myForkIO :: IO () -> IO (MVar ())
myForkIO io = do
     mvar <- newEmptyMVar
     forkFinally io (\_ -> putMVar mvar ())
     return …

假设我有两种类型:

t1 <- [t| (Functor f) => (a -> b) -> f a -> f b |]
t2 <- [t| (Int -> Char) -> [Int] -> [Char] |]

是否有可能在Template Haskell中确定表达式t1也可以是t2？(我自己没有实现类型统一.)

在启动一个新的Haskell项目时,它需要新旧扩展提供的语言功能,我应该使用哪些？新的还是旧的？例如:

• GADTs取代了存在主义的统一.
• 在许多情况下,TypeFamilies取代了FunctionalDependencies.
• 等等_{(如果你有更多的例子可以在这里添加)}

我倾向于新的,因为他们感觉更清洁,并且他们以统一的方式为语言添加更多功能.但是,较旧的编译器支持它们,它们在现有的库中使用,也许在程序员中更为人所知.

更新:如答案/评论中所述,上述"取代"关系并不完全准确.但是,我对(经常发生的)案例感兴趣,因为几个扩展可以很好地完成任务.

如果一个类有一个可变类型参数,例如Iterable[+A],声明之间是否有任何区别

def foo(bar: Iterable[_])

和

def foo(bar: Iterable[Any])

？

如果一个类具有逆变类型参数,例如Growable[-A],声明之间是否有任何区别

def foo(bar: Growable[_])

和

def foo(bar: Growable[Nothing])

？

假设我想在do-notation块中分叉一个线程,但我不关心线程id.如果我写

forkIO action

GHC发出警告

警告:do-not语句丢弃了类型的结果ThreadId.说出这个警告

_ <- forkOS action

Run Code Online (Sandbox Code Playgroud)

这是一个好主意,因为我想表明该程序正在丢弃某些结果.但是,这样一来,丢弃的东西就不明显了.我可以写

threadId <- forkIO action

但后来我们隐瞒了我们不会threadId在任何地方使用的事实,GHC正确警告

警告:已定义但未使用: threadId

似乎前置下划线解决了这两个问题:

_threadId <- forkIO action

我的问题是:根据Haskell的语言规范,使用以下划线开头的变量是合法的吗？它有多便携？它在某处记录了吗？是否鼓励这样的案例 - 记录结果被忽略？

我们如何证明continuation monad没有有效的实例MonadFix？

Data定义为其核心功能之一gfoldl:

gfoldl
  :: (Data a)
  => (forall d b. Data d => c (d -> b) -> d -> c b) 
  -> (forall g. g -> c g)   
  -> a  
  -> c a

有什么目的c和c (d -> b)它吗？为什么它不仅仅是一个常规的折叠,类似于

gfoldl'
  :: (Data a)
  => (forall d. Data d => r -> d -> r)
  -> r
  -> a  
  -> r