基本上,我想要的是一个函数,它接受一个函数类型(a - > b - > c - > ...),并返回该函数类型的所有右子集类型的列表,例如,让我们调用这个功能f:
x = f (a -> b -> c)
x
> [a -> b -> c, b -> c, c]
这应该适用于多态类型,如我的示例,以及具体的函数类型.
如果您可以在类型级别上使用函数类型进行模式匹配,那么这将是相对简单的:
g (x -> xs) = xs
g (x) = x
用作上面构造f的效用函数,并且函数类型上的模式匹配类似于在列表上进行模式匹配.
假设我Eff () [STDIO]在Idris中有类型的功能.这使您可以执行基本的控制台I/O操作,但不允许您使用Idris的外部函数接口.
在idris中是否有效果可以让你这样做,还是以其他方式解决这个问题？我不想IO在这个例子中使用,因为我希望能够将FFI与其他效果混合使用.因此,如果我想使用FFI和状态效果,例如,我希望能够使用类型:Eff () [FFI,State Int].这在Idris的当前实施中是否可行？
通常，每当在 Haskell（或任何其他语言）中使用幺半群运算符时，我发现自己在问“如果语言本身支持幺半群运算的规范化会不会很方便？允许我们在某些东西上工作像一个严格的幺半群？”
最近，我有一个想法，可以通过使用类型系列在 Haskell 中实现与此类似的东西（尽管并不完全相同，因为 ex((), a)并且a仍然是不同的类型。要了解我的意思，请考虑以下类型：
-- From Control.Arrow
(***) :: a b c -> a b' c' -> a (b, b') (c, c')
x :: MyArrow () Int
y :: MyArrow String Int
目前，这个API，结合x和y与***收益率：
x *** y :: MyArrow ((),String) (Int,Int)
但是从“幺半群”的角度来看，我真正想看到的类型是同构的：
x *** y :: MyArrow String (Int,Int)
然而，要使用标准箭头组合器实际实现这一点，需要编写：
(\x -> ((), x)) ^>> (x *** y) :: MyArrow String (Int,Int)
现在，为了绕过这个样板（假设我们不想处理这种将幺半群类型简化为正常形式的簿记），我的想法是使用类型族：
type family Reduce (pi :: …我正在为纸牌游戏制作一些代码:
splitCards_ (x:xs) (a,b,c) | isGold x = splitCards xs (a:x,b,c)
| isAction x = splitCards xs (a,b:x,c)
| isVP x = splitCards xs (a,b,c:x)
splitCards_ [] (a,b,c) = (a,b,c)
splitCards xs = splitCards_ xs ([],[],[])
基本上,取一张卡片列表,并根据卡片的类型将其分成三个不同的列表.splitCards_通过递归更新它的参数来表示状态更新,然后splitCards(实际函数)用于始终以三个特定类型的卡列表为空来开始计算.
我相信这被称为状态传递风格,我很确定这是完全惯用的,但我更关心的事实是我必须定义一个辅助函数splitCards_才能让它以我想要的方式工作.正在创建像这个惯用的Haskell一样的辅助函数吗？是否有更清晰的方式来写这个？有没有命名约定只是在辅助函数名称的末尾加上下划线？
我们需要制作一个程序来模拟我的计算机体系结构类的IEEE浮点数的划分.我几乎已经完成了这个,但我认为看看程序在APL中会是什么样子会很有趣,但据我所知,在APL中没有(直接)方式进行按位操作(按位和/或,转移等...).如果可能,在APL中执行此操作的最简单方法是什么？
我正在使用单例库在 Haskell 中编写具有多态变体的原型编程语言。我有一个基本类型的类型，如下所示：
import Data.Singletons.TH
import Data.Singletons
import GHC.Natural
import Data.Singletons.TypeLits
$(singletons [d|
data MyType =
PredT
| ProcT [MyType]
| IntT
| FloatT
| StringT
| FuncT MyType MyType
| VariantT Natural [MyType]
| UnionT [MyType]
|])
的Natural在参数VariantT被用来标识特定的变体，而对于这实际上是很重要的Natural（而不是像在NAT定义为代数数据类型）efficency原因。
问题是，有了这个定义，我得到：
Couldn't match expected type ‘Natural’
with actual type ‘Demote Natural’
通常，根据我对单例库的经验，当我尝试将类型用作单例SingKind而不支持该类型时，我会遇到这样的错误（无论如何我的理解）e.x. for Char，所以我不知道为什么会这样不工作。
我已经尝试过Demote Natural, Nat, 以及不同的导入（我想也许我没有使用正确的“Nat”或“Natural”，单身人士可以使用），所有这些都给了我类似的错误。这里有什么问题？我是否必须编写单例为 which 类型手动生成的定义Demote a != a，或者我在这里遗漏了什么？
我实际上并不认为"类型扩展"一词正式意味着我想要的东西,但这是我能想到的唯一一个词.
我有一个多态Haskell类型来表示命题逻辑中的术语:
data PropLogic a = Prop a | Tautology | Contradiction | And (PropLogic a) (PropLogic a)
| Or (PropLogic a) (PropLogic a) | Implies (PropLogic a) (PropLogic a)
| Not (PropLogic a)
deriving (Eq,Show)
问题是,我还想要一个类似的多态类型用于具有量化运算符的命题逻辑:
data PropQuantifiedLogic a = Prop a | Tautology | Contradiction | And (PropQuantifiedLogic a) (PropQuantifiedLogic a)
| Or (PropQuantifiedLogic a) (PropQuantifiedLogic a) | Implies (PropQuantifiedLogic a) (PropQuantifiedLogic a)
| Not (PropQuantifiedLogic a) | Forall (PropQuantifiedLogic a)
| Exists (PropQuantifiedLogic a)
deriving (Eq,Show)
现在,我只需要添加一个前缀的每个值构造其中两个的名字 …
我正在努力将 Haskell 中的一个简单的 prolog 实现翻译成 Rust 以获得乐趣，并获得更多使用该语言的经验。
在 Haskell 中，我有一个类型类：
class Unifiable t v | t -> v where
variables :: t -> [v]
subs :: Unifier v t -> t -> t
unify :: t -> t -> (Maybe (Unifier v t))
我在 Rust 中将其转化为以下特征：
pub type Unifier<V,T> = HashMap<V,T>;
pub trait Unifiable<T,V> {
fn variables(term: T) -> Vec<V>;
fn subs(unifier: Unifier<V,T>, term: T) -> T;
fn unify(firstTerm: T, secondTerm: T) -> Option<Unifier<V,T>>;
然后，我定义了一个实用程序函数，只要有 的实例Unifiable可用，我就可以使用它。作为初步定义，我使用了这个：
pub fn …考虑以下 Idris 中的代码片段：
myList : List Int
myList = [
1,
2,
3
]
结束定界符]与声明本身位于同一列。我发现这是一种很自然的方式来格式化长的多行列表。
但是，Haskell 中的等效代码段无法编译并出现语法错误：
myList :: [Int]
myList = [
1,
2,
3
]
>> main.hs:9:1: error:
>> parse error (possibly incorrect indentation or mismatched brackets)?
>> |
>> 9 | ]
>> | ^
并且要求将结束定界符]放置在严格大于表达式声明位置的列号上。或者至少，据我所知，这似乎是正在发生的事情。
Haskell 不喜欢这种语法有什么原因吗？我知道 Haskell 解析器和词法分析器之间存在一些微妙的交互，以启用 Haskell 的越位规则实现，所以也许它与此有关。
我正在Haskell中编写一些数据类型来表示正式的英语语法.
data S = NP VP
到目前为止,句子只是名词短语和动词短语.惊叹于代数数据类型的优雅之美!
我还将一个限定词和形容词定义为:
data D = A | An | The
type Adj = String -- Too many adjectives for me to list, so I make it a type
-- synonym for String.
现在,我遇到了定义NP的问题,这是一个带有可选限定词和形容词的名词.我的第一个天生本能是使用Maybe:
data NP = Maybe D Maybe Adj N
这给了我错误:
Expecting one more argument to `Maybe' In the type `Maybe' In the definition of data
constructor `Maybe' In the data type declaration for `NP'
(请注意,根据我是否导入了Data.Maybe,错误不会改变)
我使用它的唯一方法是使用记录语法:
data NP' = NP' {determiner :: …