小编phy*_*nfo的帖子

列表推导和地图计算都应该 - 至少在理论上 - 相对容易并行化:列表理解中的每个计算都可以独立于所有其他元素的计算来完成.例如在表达式中

[ x*x for x in range(1000) ]

每个x*x-计算可以(至少在理论上)并行完成.

我的问题是:是否有任何Python-Module/Python-Implementation/Python Programming-Trick来并行化列表理解计算(为了使用所有16​​/32/...核心或通过计算机网格分配计算或在云上)？

由于_+_-Operation for Nat通常在第一个参数中以递归方式定义,因此对于类型检查器来说,知道这一点显然是非常重要的i + 0 == i.但是,当我在固定大小的向量上编写函数时,我经常遇到这个问题.

一个例子:我如何定义Agda函数

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

它将第一个n值放在向量的末尾？

因为Haskell中的简单解决方案是

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

我在Agda中类似地尝试过这样的:

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap …

我使用ghcs扩展定义了固定长度向量GADTs,TypeOperators并且DataKinds:

data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 

infixr 3 :.

data VNat  =  VZero |  VSucc VNat  -- ... promoting Kind VNat

type T1 = VSucc VZero
type T2 = VSucc T1

以及TypeOperator的以下定义:+:

type family (n::VNat) :+ (m::VNat) :: VNat 
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n …

我想使用图形数据库用于Web应用程序(涉及用户,帖子,评论,投票,答案,文档和文档合并的网络以及用户和文档上的一些其他传递关系).所以我开始问自己是否有类似于图形数据库的设计方法,即一种类似于关系数据库推荐的设计原则(如那些普通形式)？

示例问题(出现许多问题):

• 创建一个顶级节点用户,在数据库中的任何用户节点上建立关系("存在")是一个好主意吗？
• 建立版本管理(即创建关系(类似"跟随"))是一个好主意,指向文档/帖子的更新版本,这种方式可以回退这种关系意味着观察文档所经历的更改.
• 等等...

那么,我们需要图形数据库设计手册吗？

我有两个密切相关的问题:

首先,如何在Agda中对Haskell的Arrow类进行建模/表示？

 class Arrow a where 
      arr :: (b -> c) -> a b c
      (>>>) :: a b c -> a c d -> a b d
      first :: a b c -> a (b,d) (c,d)
      second :: a b c -> a (d,b) (d,c)
      (***) :: a b c -> a b' c' -> a (b,b') (c,c')
      (&&&) :: a b c -> a b c' -> a b (c,c')

(以下博客文章指出它应该是可能的......)

其次,在Haskell中,它(->)是一流的公民,只是另一个更高阶的类型,它可以直接定义(->)为 …

我有一个Jupyter笔记本.在单元格1中,我定义了许多函数,这些函数需要在其他事情之前运行.然后在下面的单元格中,我开始呈现结果.但是,当我转换为HTML时,这种布局很难看.读者必须滚动很长时间才能看到结果,他们可能根本不关心这些功能.但我必须按顺序放置代码,因为我需要这些功能.

所以我的问题是,在点击全部运行之后,有没有办法可以控制单元格的运行顺序？或者我有办法做以下事情.我将所有函数定义放在单元格20中,然后在单元格1中,我可以说告诉Jupyter类似"运行单元格20".

只是好奇这是否可行.谢谢.

只需阅读关于模型驱动软件开发(MDSD)的(德国)Wiki文章.总结Wiki定义:

• MDSD是关于DRY原则(不要重复自己)
• MDSD是关于DSL(域特定语言)和生成器的设计
• 通过MDSD可以更简洁地描述问题(通过各个DSL的更高抽象级别).

因为我知道并使用高阶函数式编程,我想知道,我的实际问题是:MDSD是否只是一种绝望的尝试,将高阶函数式编程提供的强大功能注入(部分)编程语言/范例本身缺乏那些功能？

(或者我误解了MDSD甚至可以用来支持高阶函数编程吗？)

我有以下GADT

data Vec n a where
    T    :: Vec VZero a
    (:.) :: (VNat n) => a -> (Vec n a) -> (Vec (VSucc n) a)

使用类来模拟固定长度向量

class VNat n

data VZero
instance VNat VZero

data VSucc n
instance (VNat n) => VNat (VSucc n)

我试图在vector上编程一个append-function:

vAppend :: Vec n b -> Vec m b -> Vec nm b
vAppend T T = T   -- nonsense, -- its just a minimal def for testing purposes

类型检查器不喜欢它:

 Could not deduce (nm …

我写了一个Agda函数prefixApp,它将Vector-Function应用于向量的前缀:

split : {A : Set}{m n : Nat} -> Vec A (n + m) -> (Vec A n) * (Vec A m) 
split {_} {_} {zero}  xs        = ( [] , xs )
split {_} {_} {suc _} (x :: xs) with split xs 
... | ( ys , zs ) = ( (x :: ys) , zs )

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> …

虽然我经历了一堆 Haskell-encoding-problems-Questions，但我无法解决以下问题：

我想阅读许多不同的文本文件；文件的字符编码可能不一致，我使用的任何 readFile-Function 在读取某些文件时都会引发异常。

我试着把问题浓缩：下面的情况总结了它的核心。

import Prelude hiding (writeFile, readFile)
import qualified Text.Pandoc.UTF8 as UTF (readFile, writeFile, putStr, putStrLn)
import qualified Prelude as Prel (writeFile, readFile)
import Data.ByteString.Lazy (ByteString, writeFile, readFile)

在 ghci 中，我得到以下结果：

*Main> Prel.readFile "Test/A.txt"
*** Exception: Test/A.txt: hGetContents: invalid argument (invalid byte sequence) "\226\8364
*Main> Prel.readFile "Test/C.txt"
"\8230\n"

*Main> UTF.readFile "Test/A.txt"
"\8221\n"

*Main> UTF.readFile "Test/C.txt"
*** Exception: Cannot decode byte '\x85':      
Data.Text.Internal.Encoding.Fusion.streamUtf8: Invalid UTF-8 stream 

也许以下信息有帮助：

• 该getLocaleEncoding收益率CP1252
• 两个“有问题”的文本文件的 ByteString：

*Main> readFile "Test/A.txt" "\226\128\157\r\n" …