代数数据类型的语法与Backus-Naur Form的语法非常相似,后者用于描述无上下文语法.这让我想到,如果我们将Haskell类型检查器看作语言的解析器,表示为代数数据类型(例如,表示终端符号的nularry类型构造函数),则接受的所有语言的集合与一组上下文免费语言?另外,通过这种解释,GADT可以接受哪些正式语言?
根据我对依赖类型的了解,我认为它应该是可能的,但我以前从未在一种依赖类型的语言中看到过这样的例子,所以我不确定从哪里开始.
我想要的是形式的功能:
f : [Int] -> (Int -> Bool)
f : [Int] -> (Int -> Int -> Bool)
f : [Int] -> (Int -> Int -> Int -> Bool)
Run Code Online (Sandbox Code Playgroud)
等等...
此函数采用n的列表Ints,并返回以Int作为参数的arity n的谓词函数.在依赖类型的语言中这种事情是否可行?如何实现这样的事情?
在了解Control.ArrowHaskell的内置proc表示法时,我想到如果仅将typeclass泛化为允许通用操作而不是通用语言,则该语言可能会作为通用的单曲面类别(***用于张量和>>>合成)的eDSL很有用。的。Arrowtens :: * -> * -> *Arrow(,) : * -> * -> *
经过研究后,我发现GArrows似乎很适合我的需求。但是,链接的Garrow类型类与所谓的“ HetMet” GHC扩展捆绑在一起,并支持其他功能(暂时而言)(例如,“模式类型”)用处不大。
鉴于我希望能够使用这样的GArrow类型类而不必安装非标准的GHC扩展:
在Hackage上是否有一个实际的(有点标准化)库可以满足我对此类通用箭头类型类的需求?
有了这样的库,是否有任何方法可以使用这样的GArrow类型类并使用“通用proc”表示法,而不必准备自己的GHC扩展?(RebindableSyntax也许?)
注意:另外,我对准proc符号使用广义表示法也很好。因此,或许它不会太难修改像这样,以满足我的需求。
我希望能够使用二元运算符在haskell中组合数值函数.因此,例如,使用一元数字函数:
f*g
Run Code Online (Sandbox Code Playgroud)
应翻译为:
\x -> (f x)*(g x)
Run Code Online (Sandbox Code Playgroud)
并且类似地添加.让你自己的操作员这么做是非常简单的,但我真的很想让Num a => a -> a函数成为Num的一个实例,但我不知道该怎么做.
我也想使这个参数数量通用的,但可能是因为这是多么难以做到的元数泛型函数在Haskell太麻烦了,所以它可能只是更好地界定独立Num a => a -> a -> a,Num a => a -> a -> a -> a等...实例了一些数量相当大.
在 Haskell 中,有时为了性能人们会使用unsafeCoerce(或更安全的coerce)在具有相同内部表示的类型之间进行转换。我所知道的最常见的例子是新类型列表:
newtype Identity a = Identity a
f :: [Identity a] -> [a]
f = coerce
Run Code Online (Sandbox Code Playgroud)
现在,我在我正在处理的代码库中有两个 GADT,看起来像这样精简:
data Typ where
PredT :: Typ
ProcT :: [Typ] -> Typ
IntT :: Typ
ListT :: Typ -> Typ
data HKTyp v (f :: * -> * -> *) where
HKPredT :: HKTyp v f
HKProcT :: [HKTyp v f] -> HKTyp v f
HKIntT :: HKTyp v f
HKListT :: f v (HKTyp v f) …Run Code Online (Sandbox Code Playgroud) 我正试图绕过F-algebras,这篇文章做得非常好.我理解双重类别理论的概念,但我很难理解F-coalgebras(F-代数的对偶)如何与Haskell中的惰性数据结构相关.
F-代数用endofunctor描述,函数有:F a - > a,如果你把F a看作一个表达式就有意义,而a作为评估该表达式的结果,正如链接文章所解释的那样.
作为F-代数的对偶,F-余代数的相应函数将是 - > F a.维基百科说,F-coalgebras可以用来创建无限的,懒惰的数据结构.a - > F a functon如何创建无限的,懒惰的数据结构?另外,考虑到这一点,既然Haskell处于核心的懒惰状态,Haskell F-coalgebras中的大多数数据类型都是F-algebras?F-algebras没有被懒惰地评估?
如果数据类型(或至少是能够无限数据的数据类型)基于Haskell中的F-coalgebras,那么a - > F是一个列表函数,例如?列表的终端F-coalgebra是什么?
在Haskell中创建无限列表[1,2,3,4 ...]可能看起来像这样:
list = 1 : map (+ 1) list
Run Code Online (Sandbox Code Playgroud)
这是否以某种方式使用F-coalgebras?无限数据结构是否需要使用F-coalgebras进行惰性求值和递归的概念?我在这里错过了什么吗?
考虑以下功能:
(<.>) :: [[a]] -> [[a]] -> [[a]]
xs <.> ys = zipWith (++) xs ys
Run Code Online (Sandbox Code Playgroud)
本质上,这需要两个as 的二维数组,并将它们从左到右连接起来,例如:
[[1,2],[3,4]] <.> [[1,2],[3,4]] == [[1,2,1,2],[3,4,3,4]]
Run Code Online (Sandbox Code Playgroud)
我希望能够编写如下内容:
x = foldr1 (<.>) $ repeat [[1,2],[3,4]]
Run Code Online (Sandbox Code Playgroud)
由于Haskell的懒惰评估,这应该是有道理的,即我们应该获得:
x !! 0 == [1,2,1,2,1,2,1,2...]
x !! 1 == [3,4,3,4,3,4,3,4...]
Run Code Online (Sandbox Code Playgroud)
但是,当我尝试使用GHCi运行该示例时,要么使用foldr1或foldl1,要么得到一个非终止计算,要么是堆栈溢出。
所以我的问题是:
foldr1or或其他功能来完成我正在尝试完成的操作foldl1?(很高兴,如果我需要修改的实现<.>,只要它能计算出相同的功能)另外,请注意:我知道对于此示例,它map repeat [[1,2],[3,4]]会产生所需的输出,但是我正在寻找一种解决方案,该解决方案适用于任意无限列表,而不仅限于表单repeat xs。
让我澄清一点,我不是在谈论能够压缩任何给定源材料的算法意义上的完美压缩,我意识到这是不可能的.我想要得到的是一种能够将任何源位串编码到其绝对最大压缩状态的算法,由其的Shannon熵确定.
我相信我听说过一些关于霍夫曼编码在某种意义上最优的东西,所以我相信这个加密方案可能是基于这个,但这是我的问题:
考虑位串:a ="101010101010",b ="110100011010".
使用简单的Shannon熵,当我们将位串简单地视为0和1的符号时,这些位串应该具有完全相同的熵,但是这种方法是有缺陷的,因为我们可以直观地看到位串a具有比位串b更少的熵,因为它只是一个重复10的模式.考虑到这一点,我们可以通过计算复合符号00,10,01和11的香农熵来更好地了解源的实际熵.
这只是我的理解,我可能完全偏离基础,但从我的理解,对于一个遍历源为真正随机,对于长度为n的遍历源.所有n长度符号组的统计概率必须具有相同的可能性.
我想比标题中的问题更具体,我有三个主要问题:
使用单个位作为符号的霍夫曼编码是否会像最佳一样压缩位串,即使我们在2位符号级别分析字符串时会出现明显的模式?如果没有,可以通过循环通过霍夫曼编码的不同"级别"(抱歉,如果我在这里屠宰术语)来最佳地压缩源,直到找到最佳压缩率?在某些情况下,可以通过霍夫曼编码的不同"轮次"进一步提高压缩率吗?(首先使用5位长的符号进行霍夫曼编码,然后对4位长的符号进行霍夫曼编码?huff_4bits(huff_5bits(bitstring)))
要创建一个接受类型级自然Z,(SZ),(S(SZ))...等的类型类,您可以简单地递归声明实例:
data Z
data S a
class Type a
instance Type Z
instance Type (S a)
Run Code Online (Sandbox Code Playgroud)
是否可以基于类型级谓词创建类型类实例?例如,我希望能够说:
{-# LANGUAGE MultiParamTypeClasses #-}
class Type a b
instance Type x y when (x :+: y == 8)
Run Code Online (Sandbox Code Playgroud)
:+:类型级别添加在哪里,并且==是类型级别相等Data.Type.Equality,因此仅为最多为8的nat对创建实例.
Haskell中的符号是否与此类似?如果没有,这样的事情将如何实现?
编辑:这篇文章的灵感来自关于智能构造函数的Haskell wiki文章,其中InBounds声明了一个类型类以静态验证传递给智能构造函数的幻像类型参数是在某些范围的Nats中,智能构造函数是:
resistor :: InBounds size => size -> Resistor size
resistor _ = Resistor
Run Code Online (Sandbox Code Playgroud)
在我的例子中尝试做类似的事情(在使用leftaroundabout的答案之后)给了我一个错误:
construct :: (Type a b) => a -> b -> MyType a b
construct _ _ …Run Code Online (Sandbox Code Playgroud)