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, th
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, n
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 typ
> > 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 w
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
--
G
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 tha
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 ty
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 retur
[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. Usi
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 by
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 th
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
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
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 g
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
#x27;a -> exn) * (exn -> 'a option)
type tagged = exn
fun newtag () =
let
exception E of 'a
in
(E, fn (E x) => SOME x
| _ => NONE)
end
fun tag (f, _) x = f x
fun istagof (_, g) x = g x
end
-Dan
On Oct20, TJ wrote:
> Dan
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 t
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, s
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
.
-Dan
On Jul27, Stefan 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,
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
>
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
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
yo
> In the dependently typed setting, it's often the case that the
> "with-scrutinee" is an expression of interest precisely because it
> occurs
> in the *type* of the function being defined. Correspondingly, an
> Epigram implementation should (and the Agda 2 implementation now does)
> abstract occ
On Jul25, Claus Reinke wrote:
> although you could introduce a _convention_ by which all view functions
> are supposed to be exhaustive over their input type, the types themselves
> do not encode or check exhaustiveness. so we're talking about an informal
> promise rather than a formal guarantee.
On Jul25, apfelmus wrote:
> Dan Licata wrote:
> > There's actually a quite simple way of doing this. You make the view
> > type polymorphic, but not in the way you did:
> >
> > myzip :: Queue a -> Queue b -> Queue (a,b)
> > myzip a b = case (
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.
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 ->
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 vie
[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 ::
31 matches
Mail list logo
