把我的脚趾浸入依赖类型的水域,我在规范的"静态类型长度列表"示例中有一个裂缝.
{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
-- a kind declaration
data Nat = Z | S Nat
data SafeList :: (Nat -> * -> *) where
Nil :: SafeList Z a
Cons :: a -> SafeList n a -> SafeList (S n) a
-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x
这似乎有效:
ghci> :t Cons 5 (Cons 3 Nil) …我正在尝试编写一个函数,将表单的字符串'A=5, b=7'转换为字典{'A': 5, 'b': 7}.以下代码片段是主for循环内部发生的- 它们将字符串的单个部分转换为单个dict元素.
这可以:
s = 'A=5'
name, value = s.split('=')
d = {name: int(value)}
这不是:
s = 'A=5'
d = {name: int(value) for name, value in s.split('=')}
ValueError: need more than 1 value to unpack
为什么我不能在字典理解中解包元组？如果我得到这个工作,那么我可以轻松地将整个功能变成一个紧凑的字典理解.
python dictionary dictionary-comprehension iterable-unpacking
这是项目欧拉问题49的一个(略微混乱)尝试.
我应该直截了当地说这deque不是一个好选择!我的想法是缩小质数集来测试成员资格会导致循环加速.然而,当我意识到我应该使用a set(并且不用担心删除元素)时,我的速度提高了60倍.
from collections import deque
from itertools import permutations
from .sieve import sieve_of_erastothenes # my own implementation of the Sieve of Erastothenes
primes = deque(prime for prime in sieve_of_erastothenes(10000) if prime > 1000 and prime != 1487) # all four-digit primes except 1487
try:
while True:
prime = primes.popleft() # decrease the length of primes each time to speed up membership test
for inc in xrange(1,10000 + 1 - (2 * prime)): # …的Monad类定义了一个>>方法,该方法序列的两个一元操作:
>> :: Monad m => m a -> m b -> m b
绑定运算符>>=具有翻转参数等价物=<<; 和monadic函数组合('fish')运算符>=>和<=<.<<虽然(在Hoogling几分钟之后)似乎没有.为什么是这样？
编辑:我知道这不是什么大问题.我只是喜欢使用左指向运算符看某些代码行的方式.x <- doSomething =<< doSomethingElse只是看起来更好,箭头都是一样的,而不是x <- doSomethingElse >>= doSomething.
有没有人有从Python外部与IPython内核通信的经验？
如果我试图将消息从Python应用程序发送到IPython内核,我会使用zmq.kernelmanagerAPI.实际上,我显然需要用另一种语言编写自己的内核管理器,但是我找不到我正在寻找的有关低级消息传递协议的信息.
是否有官方规范或"备忘单"记录了在0MQ上发送的实际消息的结构？这个页面描述的是比我正在寻找的更高级别的协议......我是否必须手动拆分实现以找到我想要的内容？
我已经定义了一个自定义错误类型:
data Failure = NetworkError Message |
UserIsTooStupid Message |
InvalidOperation Message |
UnexpectedError Message
type Message = String
我正在尝试使用MonadError我的错误类型:
loadJSON :: (Aeson.FromJSON v, MonadIO m, MonadError Failure m) => URI -> m v
loadJSON uri = do
body <- liftIO $ getResponseBody =<< simpleHTTP (getRequest uri)
case Aeson.decode body of
Just json -> return json
Nothing -> throwError $ SerialisationError "Couldn't deserialise from JSON"
type URI = String
换句话说,这个函数可以返回它同时满足任何单子MonadIO和MonadError,但错误的它可以抛出的唯一类型Failure.
这无法编译,错误消息:
Non …也许这是一个愚蠢的问题.下面是一个报价的Hasochism纸:
解决此问题的一种方法是将由参数化方程给出的引理编码为Haskell函数.通常,这种引理可以编码为类型的函数:
Run Code Online (Sandbox Code Playgroud)? x1 ... xn. Natty x1 ? ... ? Natty xn ? ((l ~ r) ? t) ? t
我以为我理解了RankNTypes,但我无法理解这个命题的最后部分.我正在非正式地阅读它"给出一个需要的术语l ~ r,返回那个术语".我确信这种解释是错误的,因为它似乎导致了循环:我们l ~ r直到证明本身的结论才知道,那么我怎么能期望作为证据的假设提供一个需要的术语呢？
我本来期望一个等式证明有一个更像这样的类型:
Natty x1 ? ... ? Natty xn ? l :~: r
非正式地,"给定一堆Nattys,返回命题证明l并且r相等"(使用GHC的Data.Type.Equality).这对我来说更有意义,并且似乎与你在其他依赖类型系统中所说的一致.我猜它相当于论文中的版本,但我正在努力精神上消除这两个版本.
总之,我很困惑.我觉得我错过了一个关键的洞察力.我该怎么读这个类型((l ~ r) => t) -> t？
我是monad变换器的长期用户,第一次使用monad变换器编写器....而且我觉得我做了一些不必要的事情.
我们正在开发一个具有多个数据库表的项目,并且将该集合硬编码到不同的monad堆栈变得笨重,所以我们决定将其分解为不同的可插入monad变换器,允许我们在功能类型级别进行选择,如下所示
doSomething::(HasUserTable m, HasProductTable m)=>Int->m String
(HasXTable是类,XTableT是具体的monad变换器).这些独立的monad变压器可以完全模块化的方式插入或移除,并存储DB手柄,需要ResourceT等....
我的第一次尝试是将ReaderT包裹起来,它将用于保存数据库句柄.很明显,这是行不通的,因为ReaderT(和StateT等)不能在不使用硬编码"升力"链的情况下堆叠,从而破坏了堆叠元件的可插拔模块性.
唯一的解决方案似乎是编写完全独立的ReaderT monad副本,每个副本允许访问较低级别的其他副本.这是有效的,但解决方案充满了样板代码,就像这样
class HasUserTable m where
getUser::String->m User
newtype UserTableT m r = UserTableT{runUserTableT::String->m r}
--Standard monad instance stuff, biolerplate copy of ReaderT
instance Functor m=>Functor (UserTableT m) where....
instance Applicative m=>Applicative (UserTableT m) where....
instance Monad m=>Monad (UserTableT m) where....
instance Monad m=>HasUserTable (UserTableT m) where....
--Gotta hardcode passthrough rules to every other monad transformer
--in the world, mostly using "lift"....
instance MonadTrans BlockCacheT where....
instance (HasUserTable m, Monad m)=>HasUserTable …我无法理解函数应用程序如何与haskell中的currying一起工作.如果我有以下功能:
($) :: (a -> b) -> a -> b
我明白要部分应用这个功能,我需要提供(a -> b)函数($第一个参数).
为什么可以先应用一个值(即反向参数)？
($ 0) :: Num a => (a -> b) -> b
我在这里错过了什么？
haskell operators partial-application dollar-sign operator-sections
有没有办法说明运算符是可交换的,所以我不必为两个方向给出相同的定义？例如:
data Nat = Zero | Succ Nat
(+) :: Nat -> Nat -> Nat
Zero + x = x
x + Zero = x
...
在这里,有没有一种方法可以让我不必同时给出这两种定义,其中一种定义会从另一种定义中暗示出来？有没有办法说明这一点fn = flip fn？