我正在努力培养Haskell单身人士.
在论文Dependently Typed Programming with Singletons 和他的博客文章中,单例v0.9发布了! Richard Eisenberg定义了数据类型Nat,它用peano公理定义了自然数:
data Nat = Zero | Succ Nat
Run Code Online (Sandbox Code Playgroud)
通过使用语言扩展DataKinds,此数据类型将提升为类型级别.数据构造器Zero和Succ被提升为类型构造函数的Zero和'Succ.有了这个,我们得到每个自然数在类型级别上的单个和唯一对应类型.例如3我们得到'Succ('Succ('Succ'Zero)).所以我们现在有自然数字作为类型.
然后,他在值级别上定义函数plus,在类型级别上定义类型族Plus 以使可用的加法操作.通过单例库的提升功能/准分析器,我们可以从plus功能自动创建Plus类型系列.所以我们可以避免写自己的类型家庭.
到现在为止还挺好!
使用GADT语法,他还定义了一个数据类型SNat:
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
Run Code Online (Sandbox Code Playgroud)
基本上他只将Nat类型包装成SNat构造函数.为什么这有必要?我们获得了什么?Nat和SNat的数据类型是不同构的吗?为什么SNat是单身人士,为什么 …
haskell dependent-type type-level-computation singleton-type
Haskell有一个用于定义类型系列的resticted语法:
(1) type family Length (xs :: [*]) where
(2) Length '[] = 0
(3) Length (x ': xs) = 1 + Length xs
Run Code Online (Sandbox Code Playgroud)
在等号(=)左侧的第(2)和(3)行上,我们只有简单的模式匹配.在等号的右侧,我们只有类型级函数应用程序,作为语法糖,有类型运算符(第(3)行中的(+)).
没有防护,没有case表达式,没有if-then-else语法,没有let和where,而且没有部分函数应用程序.这不是问题,因为缺少的case表达式可以被专门的类型级别函数替换,该模式匹配不同的情况,缺少的if-then-else语法可以被Data.Type的If 函数替换. Bool 包.
查看我们看到的一些示例,类型级别上的模式匹配语法至少有一个附加功能,在普通Haskell值级别函数中不可用:
(1) type family Contains (lst :: [a]) (elem :: a) where
(2) Contains (x ': xs) (x) = 'True
(3) Contains '[] (x) = 'False
(4) Contains (x ': xs) (y) = Contains xs …
Run Code Online (Sandbox Code Playgroud) 维基百科写关于Hylomorphism:
在[...]函数式编程中,一个hylomorphism是一个递归函数,对应于一个变形的组成(首先构建一组结果;也称为'展开'),然后是一个变形(然后将这些结果折叠成一个最终回报值).将这两个递归计算融合成单个递归模式然后避免构建中间数据结构.这是砍伐森林的一个例子,这是一种计划优化策略.
(我的大胆加价)
使用递归方案库我写了一个非常简单的hylomorphism:
import Data.Functor.Foldable
main :: IO ()
main = putStrLn $ show $ hylosum 1000
hylosum :: Int -> Int
hylosum end = hylo alg coalg 1
where
-- Create list of Int's from 1 to n
coalg :: Int -> ListF Int Int
coalg n
| n > end = Nil
| otherwise = Cons n (n + 1)
-- Sum up a list of Int's
alg :: ListF Int …
Run Code Online (Sandbox Code Playgroud) 在单例包中,函数withKnownNat具有以下奇怪的类型签名:
withKnownNat :: Sing n -> (KnownNat n => r) -> r
.
所述KnownNat n =>
上下文是不是后::
(hasType)符号,但在第二个函数参数:-> (KnownNat n => r) ->
.
我如何阅读此签名?它究竟意味着什么?它在哪里记录?
如何使用检查器库来测试简单解析器的Functor定律?
import Test.QuickCheck
import Test.QuickCheck.Checkers
import Test.QuickCheck.Classes
import qualified Data.ByteString as BS
type Index = Int
newtype Parser a = Parser (BS.ByteString -> Index -> (a, Index))
runParser :: Parser a -> BS.ByteString -> Index -> (a, Index)
runParser (Parser p) = p
instance Functor Parser where
f `fmap` p = Parser $ \bs i ->
let (a, ix) = runParser p bs i
in (f a, ix)
Run Code Online (Sandbox Code Playgroud)
我想我必须使用Test.QuickCheck.Classes中的仿函数函数
类型是:
functor :: forall m a …
Run Code Online (Sandbox Code Playgroud) 使用以下代码,我想将 Data.Text 值序列化为 ByteString。不幸的是,我的文本前面添加了不必要的 NUL 字节和 EOT 字节:
GHCi, version 9.4.4: https://www.haskell.org/ghc/ :? for help
ghci> import qualified Data.Text as T
ghci> import Data.Binary
ghci> import Data.Binary.Put
ghci> let txt = T.pack "Text"
ghci> runPut $ put txt
"\NUL\NUL\NUL\NUL\NUL\NUL\NUL\EOTText"
ghci>
Run Code Online (Sandbox Code Playgroud)
问题:
PS:我真正的代码我把长度放在文本前面
foo :: Text -> ByteString
foo txt = runPut do
putWord32host $ T.length txt
put txt
Run Code Online (Sandbox Code Playgroud) 这是Acess的一个跟进问题,一个带有reflex-dom客户端的servant服务器:
如果我在Web浏览器中运行客户端代码,一切正常.但是,如果我在gtk3(和Debian)下运行webkit中的客户端代码,我可以在服务器中看到请求,但客户端没有收到任何响应.
我想,这又是某种安全性或CORS问题.我发现这篇文章如何从2012年开始禁用webkit gtk中的web安全性(跨源reequest),因为这个bug 不可能https://bugs.webkit.org/show_bug.cgi?id=58378.如果我看看这个bug,它会说:状态:已解决固定.提到的SO帖子的第二个答案显示了未指定文件中的一些设置.
我的问题是:在哪里(目录和文件),我必须说明什么,从WebkitGtk客户端访问服务器.
作为非 nix'er,我安装了最新版本的https://github.com/reflex-frp/reflex-platform。我认为在这个 nix-shell 中工作是一次很好的体验。
现在我想知道这个 shell 中安装和使用了哪些版本的 Haskell 软件包。经过一番谷歌搜索后,我发现了一个如下形式的nix-env命令:
nix-env -f '<nixpkgs>' -qaPA haskellPackages|grep reflex-dom
该命令为我提供了 reflex-dom 的版本为reflex-dom-0.3。但我从这里知道,在我的 nix shell 中,我使用的是最新版本的 reflex-dom 0.4 。所以我假设上面的命令只是列出了可用的 Hackage 包。
仅获取已安装的 Haskell 软件包及其版本的正确nix-env -q命令是什么?
(我使用了 --installed 选项,但我从未得到任何回报)
使用递归方案库,可以轻松编写抽象语法树和相应的表达式计算器:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
import Data.Functor.Foldable
import Data.Functor.Foldable.TH
data Expr = Plus Expr Expr
| Mult Expr Expr
| Const Expr
deriving (Show, Eq)
makeBaseFunctor ''Expr
-- Write a simple evaluator
eval :: Expr -> Int
eval = cata alg
where
alg = \case
PlusF x y -> (+) x y
MultF x y -> (*) x …
Run Code Online (Sandbox Code Playgroud) 这里有一些简单的F代数用于列表.他们与工作cata
从函数
的递归的方案库.
import Data.Functor.Foldable
algFilterSmall :: ListF Int [Int] -> [Int]
algFilterSmall Nil = []
algFilterSmall (Cons x xs) = if x >= 10 then (x:xs) else xs
algFilterBig :: ListF Int [Int] -> [Int]
algFilterBig Nil = []
algFilterBig (Cons x xs) = if x < 100 then (x:xs) else xs
algDouble :: ListF Int [Int] -> [Int]
algDouble Nil = []
algDouble (Cons x xs) = 2*x : xs
algTripple :: ListF Int [Int] -> …
Run Code Online (Sandbox Code Playgroud) haskell ×10
syntax ×2
boilerplate ×1
bytestring ×1
ghc ×1
gtk3 ×1
nix ×1
quickcheck ×1
reflex ×1
webkit ×1
webkitgtk ×1