我正在构建一个Haskell程序,该程序使用命令行参数解析器使用option-applicative库.由于我使用堆栈来构建和测试我的项目,我想使用stack exec执行我的程序传递命令行参数,就像
stack exec myprogram-exe -i myfile.txt
但是当我尝试执行时,Stack给了我以下消息:
Usage: stack exec CMD [-- ARGS (e.g. stack ghc -- X.hs -o x)] ([--plain] |
([--ghc-package-path] | [--no-ghc-package-path])
([--stack-exe] | [--no-stack-exe]) [--package ARG])
有没有办法可以将命令行参数传递给使用Stack执行的程序？
我想为以下数据类型开发一个类型安全查找函数:
data Attr (xs :: [(Symbol,*)]) where
Nil :: Attr '[]
(:*) :: KnownSymbol s => (Proxy s, t) -> Attr xs -> Attr ('(s , t) ': xs)
明显的查找功能如下:
lookupAttr :: (KnownSymbol s, Lookup s env ~ 'Just t) => Proxy s -> Attr env -> t
lookupAttr s ((s',t) :* env')
= case sameSymbol s s' of
Just Refl -> t
Nothing -> lookupAttr s env'
其中Lookup类型族在单例库中定义.此定义无法在GHC 7.10.3上键入检查,并显示以下错误消息:
Could not deduce (Lookup s xs ~ 'Just …我正在尝试使用并行抢占式调度来编写IMP语言的功能语义,如下文第4部分所述.
我正在使用Agda 2.5.2和标准库0.13.此外,整个代码可以通过以下要点获得.
首先,我将所讨论语言的语法定义为归纳类型.
data Exp (n : ?) : Set where
$_ : ? ? Exp n
Var : Fin n ? Exp n
_?_ : Exp n ? Exp n ? Exp n
data Stmt (n : ?) : Set where
skip : Stmt n
_?_ : Fin n ? Exp n ? Stmt n
_?_ : Stmt n ? Stmt n ? Stmt n
iif_then_else_ : Exp n ? Stmt n ? Stmt …我正在尝试使用Idris接口实现一个简单的代数结构层次结构.代码如下:
module AlgebraicStructures
-- definition of some algebraic structures in terms of type classes
%access public export
Associative : {a : Type} -> (a -> a -> a) -> Type
Associative {a} op = (x : a) ->
(y : a) ->
(z : a) ->
(op x (op y z)) = (op (op x y) z)
Identity : {a : Type} -> (a -> a -> a) -> a -> Type
Identity op v = ((x : a) -> …我正在尝试为Setoids建模Agda风格的等式推理证明(具有等价关系的类型).我的设置如下:
infix 1 :=:
interface Equality a where
(:=:) : a -> a -> Type
interface Equality a => VerifiedEquality a where
eqRefl : {x : a} -> x :=: x
eqSym : {x, y : a} -> x :=: y -> y :=: x
eqTran : {x, y, z : a} -> x :=: y -> y :=: z -> x :=: z
使用这样的接口,我可以模拟一些像Syntax.PreorderReasoning伊德里斯库那样的等式推理组合器
.
syntax [expr] "QED" = qed expr
syntax [from] "={" [prf] "}=" [to] …我在Idris中玩一些形式化的游戏，并且有一些奇怪的行为：函数的编译时间和CPU使用率很高。
该代码是一个正则表达式模式匹配算法。首先是正则表达式定义：
data RegExp : Type where
Zero : RegExp
Eps : RegExp
Chr : Char -> RegExp
Cat : RegExp -> RegExp -> RegExp
Alt : RegExp -> RegExp -> RegExp
Star : RegExp -> RegExp
Comp : RegExp -> RegExp
正则表达式的成员资格和非成员资格定义为以下相互递归的数据类型：
mutual
data NotInRegExp : List Char -> RegExp -> Type where
NotInZero : NotInRegExp xs Zero
NotInEps : Not (xs = []) -> NotInRegExp xs Eps
NotInChr : Not (xs = [ c ]) -> NotInRegExp xs …假设我想要定义由两个类型级环境索引的数据类型.就像是:
data Woo s a = Woo a | Waa s a
data Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) =
Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') }
这个想法是env输入环境,env'是输出环境.因此,type Foo类似于索引状态monad.到现在为止还挺好.我的问题是我怎么能表明这Foo是一个应用函子.显而易见的尝试是
instance Applicative (Foo s env env') where
pure x = Foo (\s env -> (Woo x, env))
-- definition of (<*>) omitted.
但GHC抱怨pure说它是错误类型的,因为它推断了类型
pure :: …我正在尝试在Haskell中使用依赖类型编程的一些实验,但没有成功.我的想法是在有限映射上表达某种弱化属性.整个代码如下:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Exp where
import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits
data Exp (env :: [(Symbol,*)]) (a :: *) where
Val :: Int -> Exp env Int
Var :: (KnownSymbol s, Lookup s env ~ 'Just a) …我正在学习 Idris 并且我陷入了一个非常简单的引理，该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式，但 Idris 拒绝使用以下错误消息：
RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case
完整的代码片段可在以下要点中找到：
https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee
任何帮助表示赞赏。
I'm designing a DSL in Haskell and I would like to have an assignment operation. Something like this (the code below is just for explaining my problem in a limited context, I didn't have type checked Stmt type):
data Stmt = forall a . Assign String (Exp a) -- Assignment operation
| forall a. Decl String a -- Variable declaration
data Exp t where
EBool :: Bool -> Exp Bool
EInt :: Int -> Exp Int
EAdd :: Exp Int …