Hi everyone,
Yes, the current overlap checker thinks all view patterns are
overlapped. The pattern overlap/exhaustiveness checker needs to be
rewritten to account for GADTs and view patterns.
You can use -fno-warn-overlapping-patterns to suppress these warning
(along with any actual overlaps,
On Mar12, [EMAIL PROTECTED] wrote:
G'day all.
Quoting David Menendez [EMAIL PROTECTED]:
Adrian is arguing that compare a b == EQ should imply compare (f a) (f
b) == EQ for all functions f (excluding odd stuff). Thus, the problem
with your example would be in the Ord instance, not the sort
Hi Ryan,
On Feb13, Ryan Ingram wrote:
However, you can express exists in terms of forall:
exists x, P(x) is equivalent to (not (forall x, not P(x)))
that is, if it is not true for all x that P(x) does not hold, then
there must be some x for which it does hold.
The existential types
And finally, vector, which is supposed to build a fixed-sized vector
out of a list.
The ideal type for the function would be:
vector :: [a] - FSVec s a
But there is no apparent way in which to obtain s based on the length
of the input list.
[1] shows a way in which to create
Out of context (am I missing some earlier part of this thread?) I'm not
entirely sure what you mean.
Are you're talking about the disjunction elim rule in intuitionistic
natural deduction:
Gamma |- A + B Gamma, A |- C Gamma, B |- C
--
Hi Bulat,
Once again, let's be careful about what check arbitrary functions for
termination/non-trivialness means. If you mean, decide via an
algorithm whether a function is terminating on all inputs, then yes,
you need to restrict the class of functions. If you mean prove in some
logic that a
On Feb06, Henning Thielemann wrote:
On Tue, 5 Feb 2008, Dan Licata wrote:
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2
Let's be careful here: decidability is only relevant if you want to
*automatically* prove calls to filter correct. It is certainly possible
to give a type system/specification logic for reasoning about all
functions written in a Turing-complete language (e.g., all Haskell
functions). In such a
[CC'ed to the agda mailing list as well]
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
will always compute an empty list. Using an
Not to start a flame war or religious debate, but I don't think that
eta-expansions should be considered bad style. I realize that
composition-style is good for certain types of reasoning, but fully
eta-expanded code has an important legibility advantage: you can tell
the shape of its type just
On Jan27, Dipankar Ray wrote:
What I mean by this is that if I look at the CS programs at Berkeley, MIT,
CMU, I don't see a huge emphasis on PL. Looking now at the MIT
opencourseware offerings in EECS, I see no undergrad course that suggests
that you'd learn anything about modern type
See also
A parallel, real-time garbage collector
Perry Cheng and Guy Blelloch
PLDI 2001
This was implemented in the TILT compiler for SML (which, to be fair, is
more of a research vehicle than a programmer-friendly implementation).
-Dan
On Jan25, Stefan Kersten wrote:
On 25.01.2008, at
A further plug:
I did an internship with Simon PJ last summer (implementing view
patterns in GHC, among other things), and this is a great opportunity if
you're interested in PL research. There is a lot of interesting work
going on at MSR Cambridge, the atmosphere is very friendly, and
Cambridge
On Jan24, Antoine Latter wrote:
Can Fix be made to work with higher-kinded types? If so, would the
following work:
Yes, it can.
For a particular A (e.g., Int), List A is a recursive type
Fix X. 1 + (A * X).
List :: type - type is a family of recursive types: if you give it a
type, it gives
On Nov08, Simon Peyton-Jones wrote:
| Windows and Haskell is not a well travelled route, but if you stray of
| the cuddly installer packages, it gets even worse.
|
| But it shouldn't. Really it shouldn't. Even though Windows is not my
| preferred platform, it is by no means different enough
fun tag (f, _) x = f x
fun istagof (_, g) x = g x
end
-Dan
On Oct20, TJ wrote:
Dan Licata: Thanks for explaining the mechanics behind it. Knowing how
it (could) be implemented always helps me understand things.
On 10/20/07, Jules Bean [EMAIL PROTECTED] wrote:
Quite often an explicit
You've almost got it right below. Here's an example of using existentials:
{-# OPTIONS -fglasgow-exts #-}
data AnyNum where
E :: forall a. Num a = a - AnyNum
l :: [AnyNum]
l = [E (1 :: Integer), E (2.0 :: Float)]
neg :: [AnyNum] - [AnyNum]
neg = map (\ (E x) - E (0 - x))
-- testing:
Another way of understanding the terminology is this:
A dependent product type (usually written \Pi x:A.B) can be thought of
as a big product of the types (B[a1/x], ..., B[aN/x]) for the
inhabitants a1...aN of the type A. To introduce a dependent product, you
have to provide each component of
Hi Chris,
Simon mentioned this to me as a possible project when I started my
internship here at MSR, so I'm pretty sure this is both on the wish-list
and not already taken (but we should check with Simon to make sure).
I've since wished for it a few times as I've been implementing view
patterns,
O'Rear wrote:
On Fri, Jul 27, 2007 at 05:22:37AM -0400, Dan Licata wrote:
On Jul26, Stefan O'Rear wrote:
So, this syntax affects a lot of code, existing or otherwise, that
doesn't use view patterns, which is something we're trying to avoid.
Eh? I *think* the typing rules
On Jul30, Claus Reinke wrote:
one could turn that promise into a type-checked guarantee by using
explicit sum types (and thus structural rather than name-based typing),
but that gets awkward in plain haskell.
I don't think the choice of whether you label your variants with names
or with
On Jul26, Stefan O'Rear wrote:
So, this syntax affects a lot of code, existing or otherwise, that
doesn't use view patterns, which is something we're trying to avoid.
Eh? I *think* the typing rules are the same for the no-view case. If
the auto-deriving hack isn't implemented, you only
On Jul26, apfelmus wrote:
Yes, the types of the patterns don't unify. But each one is a
specialization of the argument type. Note that the type signature is
bar :: (forall a . ViewInt a = a) - String
which is very different from
bar :: forall a . ViewInt a = a - String
Without
I think what you're describing is equivalent to making the implicit
view function syntax so terse that you don't write anything at all. So
the pattern 'p' is always (view - p). This seems like a pretty
invasive change:
I don't think the version with the functional dependency works (unless
you
[I think we should move the rest of this thread to haskell-cafe, since
it's getting long. Note that there have already been some responses on
both lists.]
Hi Claus,
On Jul25, Claus Reinke wrote:
I think that the signature
type Typ
unit :: Typ - Maybe ()
arrow :: Type - Maybe
Hi Conor,
This is a really good point, especially in the presence of GADTs and
type-level functions and so on, which introduce aspects of dependency.
Why are you so fatalistic about with in Haskell? Is it harder to
implement than it looks? It seems to be roughly in the same category as
our view
On Jul25, apfelmus wrote:
The point is to be
able to define both zip and pairs with one and the same operator : .
There's actually a quite simple way of doing this. You make the view
type polymorphic, but not in the way you did:
type Queue elt
empty :: Queue elt
cons :: elt -
On Jul25, Benjamin Franksen wrote:
Dan Licata wrote:
On Jul25, apfelmus wrote:
The point is to be
able to define both zip and pairs with one and the same operator : .
There's actually a quite simple way of doing this. You make the view
type polymorphic, but not in the way you
28 matches
Mail list logo
