(Universidade de Brasilia - Brazil)
- Liron Cohen (Cornell University - USA)
- Dominique Devriese (Vrije Universiteit Brussel - Belgium)
- Jean-Christophe Filliâtre (CNRS - France)
- Adam Grabowski (University of Bialystok - Poland)
- Warren Hunt (University of Texas - USA)
- Ori Lahav (Tel
==
Program Chair
Catalin Hritcu Inria Paris
Members
Amal Ahmed Inria Paris and Northeastern University
Lars BirkedalAarhus University
Dominique Devriese KU Leuven
Cédric Fournet Microsoft Research
Deepak Garg MPI-SWS
Xavier Leroy Inria
using F*, C/C++ and X64.
Anitha Gollamudi, Cédric Fournet.
Constant-time WebAssembly. John Renner, Sunjay Cauligi, Deian Stefan.
Enforcing Well-bracketed Control Flow and Stack Encapsulation using
Linear Capabilities. Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Formally Secure
University
Lars BirkedalAarhus University
Dominique Devriese KU Leuven
Cédric Fournet Microsoft Research
Deepak Garg MPI-SWS
Xavier Leroy Inria Paris
David NaumannStevens Institute of Technology
Marco Patrignani MPI-SWS
Frank Piessens
University
Lars BirkedalAarhus University
Dominique Devriese KU Leuven
Cédric Fournet Microsoft Research
Deepak Garg MPI-SWS
Xavier Leroy Inria Paris
David NaumannStevens Institute of Technology
Marco Patrignani MPI-SWS
Frank Piessens
BirkedalAarhus University
Dominique Devriese KU Leuven
Cédric Fournet Microsoft Research
Deepak Garg MPI-SWS
Xavier Leroy Inria Paris
David NaumannStevens Institute of Technology
Marco Patrignani MPI-SWS
Frank Piessens KU Leuven
As an outsider, I would like to suggest thinking about MonoLocalBinds. GHC
has a rather convincing story (at least to me) that "(local) let should not
be generalised" (since it becomes problematic in combination with several
other language extensions) and the journal version of the OutsideIn(X)
Merijn,
Perhaps only for the sake of discussion: have you considered doing
something at the type-level instead of using TH? I mean that you could
change the type of 42 from `forall a. Num a = a` to `forall a.
HasIntLiteral a '42 = a` where HasIntegerLiteral is a type class of
kind `* - 'Integer -
Hi Merijn,
2015-02-06 13:45 GMT+01:00 Merijn Verstraaten mer...@inconsistent.nl:
I don't see how that would replace the usecase I describe?
I've written out the Even use case a bit, to hopefully clarify my
suggestion. The code is a bit cumbersome and inefficient because I
can't use GHC
2015-02-06 14:20 GMT+01:00 Adam Gundry a...@well-typed.com:
It seems to me that what you would describe would work, and the
avoidance of TH is a merit, but the downside is the complexity of
implementing even relatively simple validation at the type level (as
opposed to just reusing a
Perhaps an alternative for this could be extending McBride's idiom brackets:
https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/idiom.html
with a form of top-level let, something like:
(| let x = expr1
y = expr2
z = expr3
in x*y + y*z + z*x |)
=
pure (\x y z - x*y + y*z
Simon,
I see your point. Essentially, the original proposal keeps the
namespace for field names syntactically distinguishable from that of
functions, so that the type given to r.foo doesn't depend on what is
in scope. (.foo) is always defined and it is always a function of
type (r { foo::t }) =
Simon,
Yes, your summary is exactly what I meant.
2013/6/26 Simon Peyton-Jones simo...@microsoft.com:
In fact, your observation allows us to regard our proposal as consisting of
two entirely orthogonal parts
* Generalise the type of record field selectors
* Introduce period as reverse
Richard,
Thanks for your answers.
2013/6/24 Richard Eisenberg e...@cis.upenn.edu:
The nub of the difference is that type families can pattern-match on kinds,
whereas term-level functions cannot pattern-match on types. So, while the @a
is repeated in the pattern as written above, GHC does
I think it's a good idea to push forward on the records design because
it seems futile to hope for an ideal consensus proposal.
The only thing I dislike though is that dot notation is special-cased to
record projections. I would prefer to have dot notation for a
general, very tightly-binding
Richard,
I'm interested by your argument at the bottom of the wiki page about
the alternative (non-)solution of disallowing non-linear patterns
altogether. I'll quote it for reference:
One way we (Simon, Dimitrios, and Richard) considered proceeding was
to prohibit nonlinear unbranched
Hi all,
I often find myself needing the following definitions:
mapPair :: (a - b) - (c - d) - (a,c) - (b,d)
mapPair f g (x,y) = (f x, g y)
mapFst :: (a - b) - (a,c) - (b,c)
mapFst f = mapPair f id
mapSnd :: (b - c) - (a,b) - (a,c)
mapSnd = mapPair id
But they seem missing from the
2013/5/28 Tikhon Jelvis tik...@jelv.is:
These are present in Control.Arrow as (***), first and second respectively.
Right, thanks. Strange that neither Hayoo nor Hoogle turned these up..
Dominique
___
Haskell-Cafe mailing list
All,
2013/3/13 o...@okmij.org:
So, Code is almost applicative. Almost -- because we only have a
restricted pure:
pureR :: Lift a = a - Code a
with a Lift constraint. Alas, this is not sufficient for realistic
parsers, because often we have to lift functions, as in the example of
2013/3/13 Dominique Devriese dominique.devri...@cs.kuleuven.be:
class ProductionRule p = LiftableProductionRule p where
epsilonL :: a - Q Exp - p aSource
and associated
epsilonLS :: (Lift v, LiftableProductionRule p) = v - p v
epsilonLS v = epsilonL v $ lift v
Note that the point
2013/2/26 Martin Drautzburg martin.drautzb...@web.de:
I wonder if I can enforce the nonNr property somehow, i.e. enforce the rule
will not consider the same nonterminal again without having consumed any
input.
You might be interested in this paper:
Danielsson, Nils Anders. Total parser
All,
Many (but not all) of the parsing algorithms that support left
recursion cannot be implemented in Haskell using the standard
representation of recursion in parser combinators. The problem
can be avoided in Scala because it has imperative features like
referential identity and/or mutable
Andreas,
2012/11/1 Andreas Abel andreas.a...@ifi.lmu.de:
Hello,
maybe someone has experience in publishing papers that use lhs2TeX and
unicode characters with ACM, and has been in my situation before...
Sheridan, who publishes for ACM, does not like T3 fonts. However, lhs2tex
--agda does
Евгений,
The possible extension may look somehow like this:
class Applicative a = Branching a where
branch :: a (Either b c) - (a b - a d) - (a c - a d) - a d
What about the following alternative that does not require an extension?
import Control.Applicative
eitherA :: Applicative f =
Patrick,
-- Class with functional dependency
class QUEUE_SPEC_CLASS2 a q | q - a where
newC2 :: q a -- ??
sizeC2 :: q a - Int
restC2 :: q a - Maybe (q a)
insertC2 :: q a - a - q a
The above is a reasonable type class definition for what you seem to intend.
-- Without
Hi,
2012/7/21 C Gosch ch.go...@googlemail.com:
I am trying to use the TLS package from hackage, and it works fine so
far -- except when a client wants to
do session resumption (note I am not an expert in TLS, so it might be
something quite simple).
In that case, I get an alert, unexpected
2012/6/27 Tillmann Rendel ren...@informatik.uni-marburg.de:
MightyByte wrote:
Of course every line of your program that uses a Foo will change if you
switch
to IO Foo instead.
But we often have to also change lines that don't use Foo at all. For
example, here is the type of binary trees
David,
The easiest solution is probably to use multi-line string literals and
line-wrap manually:
\begin{code}
cyphertext = rlkmlj, zlnift ekblvke pqc elvm if pzlp gblrk, akrlomk zk zle \
lfpiriglpke pzlp, if pzk flpojlb rcojmk cs knkfpm, morz qcobe ak pzk rcfeorp \
cs nkjriftkpcjiu, bklnkm
2012/1/16 Yin Wang yinwa...@gmail.com:
The typical example would be
instance Eq a = Eq [a] where
[] == [] = True
(a : as) == (b : bs) = a == b as == bs
_ == _ = False
It can handle this case, although it doesn't handle it as a parametric
instance. I suspect that we don't need the
Yin,
2012/1/14 Yin Wang yinwa...@gmail.com:
On Sat, Jan 14, 2012 at 2:38 PM, Dominique Devriese
dominique.devri...@cs.kuleuven.be wrote:
I may or may not have thought about it. Maybe you can give an example
of parametric instances where there could be problems, so that I can
figure out
Yin,
2012/1/12 Yin Wang yinwa...@gmail.com:
I have an idea about type classes that I have been experimenting. It
appears to be a generalization to Haskell’s type classes and seems to
be doable. It seems to related the three ideas: type classes, implicit
parameters, and (typed) dynamic
All,
In case anyone is interested, I just want to point out an interesting
article about the relation between Haskell type classes and C++
(overloading + concepts):
http://sms.cs.chalmers.se/publications/papers/2008-WGP.pdf
Dominique
2011/10/3 Ketil Malde ke...@malde.org:
sdiy...@sjtu.edu.cn
It's not the same as what you propose, but it's related, so for
discussion, I just want to point out idiom brackets (an analog for
do-notation for Applicative functors) which have been introduced in
some Haskell-related languages. Examples are Idris
2011/6/9 Stephen Tetley stephen.tet...@gmail.com:
On 9 June 2011 09:02, Yves Parès limestr...@gmail.com wrote:
Were templates an original feature of C++ or did they appear in a revision
of the langage ?
Because C++ appeared in 1982 and Haskell in 1990.
Templates were a later addition to C++.
Robert,
2011/5/16 Robert Clausecker fuz...@gmail.com:
I found out, that GHC implements typeclasses as an extra argument, a
record that stores all functions of the typeclass. So I was wondering,
is there a way (apart from using newtype) to pass a custom record as the
typeclass record, to
2011/5/3 Manuel M T Chakravarty c...@cse.unsw.edu.au:
Interestingly, today (at least the academic fraction of) the Haskell
community appears to hold the purity of the language in higher
regard than its laziness.
I find Greg Morissett's comment on Lennart Augustsson's article pro
lazy
2011/5/2 Ketil Malde ke...@malde.org:
There is a particular reason why monads had to arise in Haskell,
though, which is to defeat the scourge of laziness.
My own view is/was that monads were so successful in Haskell since it
allowed writing flexible programs with imperative features,
Kashyap,
2011/2/11 C K Kashyap ckkash...@gmail.com:
I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?
I know that static typing and strong typing of Haskell eliminate a whole
class of problems - is that related to the proving
Also, is there any news yet on a procedure for community members with
accounts on projects.haskell.org to get access to them again? My ssh
publickey login is no longer being accepted. I had an account mainly
for hosting the darcs repo and the website for my project
grammar-combinators. The website
Also, is there any news yet on a procedure for community members with
accounts on projects.haskell.org to get access to them again? My ssh
publickey login is no longer being accepted. I had an account mainly
for hosting the darcs repo and the website for my project
grammar-combinators. The website
Hi,
I'm also curious about this. Is a pure programming style like
Haskell's less or more natural than an imperative mutable-state based
one to kids without experience. I intuitively expect that for kids
with a high-school background in mathematics would find the first more
natural, but this is
All,
2010/12/27 Jonathan Geddes geddes.jonat...@gmail.com:
I see TH used most for the following tasks:
#1 Parse a string at compile-time so that a custom syntax for
representing data can be used. At the extreme, this data might even
be an EDSL.
#2 Provide instances automatically.
Just a
Hi all,
I have a problem with the design of the Applicative type class, and
I'm interested to know people's opinion about this.
Currently, the Functor and Applicative type class are defined like this:
class Functor f where
fmap:: (a - b) - f a - f b
class Functor f =
Romain,
2010/10/25 Romain Demeyer r...@info.fundp.ac.be:
I'm working on static verification in Haskell, and I search for existing
works on specification of Haskell programs (such as pre/post conditions, for
example) or any other functional language. It would be great if there exists
a prover
2010/10/12 o...@okmij.org:
An alternative approach to model sharing at the object level is the
technique I use for modelling context-free grammars in my PADL 2011
paper Explicitly Recursive Grammar Combinators... Using ideas from
the Multirec generic programming library and some recent
John, Oleg,
2010/10/9 o...@okmij.org:
So here's a very simple expression:
t1 = let v = sigGen (cnst 1) in outs v v
which is what led to my question. I'm binding the sigGen to 'v' to
introduce sharing at the meta-level. Would it be better to introduce
support for this in the dsl?
Often
Mauricio,
2010/10/6 Maurício CA mauricio.antu...@gmail.com:
I've been working in a tool that reads a grammar with associated
actions and act on input based on that grammar. I would like to
rewrite it in a functional style, but I've not been able to find a
theory that would handle any
2010/10/5 N. Raghavendra ra...@mri.ernet.in:
At 2010-10-03T22:45:30+02:00, Dominique Devriese wrote:
comma :: (a - b) - (a - c) - a - (b,c)
comma f g x = (f x, g x)
comma = liftA2 (,)
blowup = (uncurry (++)) . liftA2 (,) (blowup . allButLast) lastToTheLength
I tried both of them
One question I have is whether I can eliminate points in the above
definition of blowup, and write something like
blowup = (++) . (blowup . allButLast, lastToTheLength)
thinking of (++) as a function String x String - String.
Actually (++) is of type String - String - String. When you
Gregory,
2010/10/3 Gregory Crosswhite gcr...@phys.washington.edu:
On 10/3/10 1:45 PM, Dominique Devriese wrote:
Additionally, you can't combine the functions (blowup . allButLast)
and lastToTheLength into a function that returns a pair like you seem
to attempt. You need a function like
Paolo,
The problem with mult is that k is not specified unambiguously. You either
need v to determine k (which is probably not what you want, at a guess), mult
to take a dummy argument that determines what k is:
[...]
or, to make Tensor a data family instead of a type family.
What is the
The grammar-combinators library is a parsing library employing a novel
grammar representation with explicit recursion. The library features
much of the power of a parser generator like Happy or ANTLR, but with
the library approach and most of the benefits of a parser combinator
library. Grammars
The grammar-combinators library is a parsing library employing a novel
grammar representation with explicit recursion. The library features
much of the power of a parser generator like Happy or ANTLR, but with
the library approach and most of the benefits of a parser combinator
library. Grammars
Some snippets from the Tutorial [1] to give an idea of the
grammar-combinator library's approach, its functional style and its
additional power (e.g. the transformations used):
Defining a simple expresssions grammar:
grammarArith :: ExtendedContextFreeGrammar ArithDomain Char
grammarArith
Johannes,
(sorry for the double mail)
I will give some short answers below, but you can find more details in
the paper we are submitting to PADL 2011 [1].
2010/9/8 Johannes Waldmann waldm...@imn.htwk-leipzig.de:
.. grammar-combinator library's approach ..
am I reading this correctly: in the
Johannes,
2010/9/8 Johannes Waldmann waldm...@imn.htwk-leipzig.de:
That compilation process is highly nonlocal
and would never be possible with, e.g., the Parsec approach.
Pipe dream: attach such a grammar object to every Parsec parser,
and include the compiler with the combinators,
and
2010/8/17 Luc TAESCH luc.tae...@googlemail.com:
May I ask you how you redact your answers and which toolchain you are using?
You can use footnote-mode [1] for easily producing the
footnotes/references if you're an emacs user.
Dominique
Footnotes:
[1]
2010/7/26 Ryan Ingram ryani.s...@gmail.com:
There are two types of datatype contexts; haskell'98 contexts (which I
think are terrible), and GHC existential contexts (which I like):
See also GADT-style data type declarations [1] and full GADT's [2],
which both behave like GHC existential
Hi,
2010/7/13 Gregory Crosswhite gcr...@phys.washington.edu:
Just out of curiosity, what work is being done in the data parallel
haskell / repa projects regarding cache locality?
Hi,
I'm not knowledgeable at all about this, but for a technical
introduction to DPH, I found the following
59 matches
Mail list logo