inars, user groups, etc
Thanks
- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Thanks, that looks useful! :)
> On 04 Oct 2013, at 17:13, Erlend Hamberg wrote:
>
> While re-reading Brent Yorgey's Excellent Typeclassopedia I converted it
> to Pandoc Markdown in order to be able to create an EPUB version. Having
> a “real” e-book meant that I could comfortably read it on my e
Interesting. It's similar in spirit to basically a safe Coerce typeclass,
but for * -> * types.
class Coerce a b where
coerce :: a -> b
class Coerce1 f g where
coerce1 :: f a -> g a
-- Dan Burton
On Tue, Oct 1, 2013 at 11:00 AM, John Wiegley wrote:
&g
Apparently that element is generated by the wiki software, since most pages
want the "view source / history" buttons above the rest of the content.
jQuery('#mw-content-text > p:first').hide()
-- Dan Burton
On Tue, Oct 1, 2013 at 8:17 AM, Dan Burton wrote:
> The of
The offending HTML is on line 93:
When I delete this paragraph element from the DOM, the ugly white bar goes
away.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
tentsForm
Could you abstract `serverSide` out into a typeclass, such as
ApplicativeIO? Sure. but why bother? The point is, you've got the
specialization you need already.
-- Dan Burton
On Tue, Oct 1, 2013 at 1:20 AM, Tom Ellis <
tom-lists-haskell-cafe-2...@jaguarpaw.co.uk> wrote:
&g
Will there be a video of the live premier?
On Fri, Sep 20, 2013 at 12:14 PM, Mark Lentczner
wrote:
> Some might remember me asking about music packages a while back... An
> update:
>
> I ended up using Euterpea, which in turn uses both Codec.Midi and
> Sound.PortMidi. My working environment was
rsion would use twice as much memory
as allPairs3.
See also:
http://www.haskell.org/haskellwiki/Tail_recursion
Here's a fun alternative for you to benchmark, using an old trick. I kind
of doubt that this one will optimize as nicely as the others, but I am by
no means an optimization guru:
a
ns/3.9.0.2/doc/html/Control-Lens-Iso.html#v:involuted
-- Dan Burton
On Sat, Aug 17, 2013 at 1:43 PM, Dan Burton wrote:
> This is indeed a job for lens, particularly, the Iso type, and the "under"
> function. Lens conveniently comes with a typeclassed isomorphism called
> "
This is indeed a job for lens, particularly, the Iso type, and the "under"
function. Lens conveniently comes with a typeclassed isomorphism called
"reversed", which of course has a list instance.
>>> under reversed (take 10) ['a'.. 'z']
"qrstu
appear during the execution of the Arrow are
> also in scope.
This really helped solidify the idea in my head that the "shape of the
factory" only makes static choices, because all of the Arrow-y "processing"
happens between <- and -<
-- Dan Burton
On Fri, Aug
, you also have an
automatic instance for Applicative, which I brought up about a month ago on
reddit:
http://www.reddit.com/r/haskell/comments/1ivd23/default_functor_and_applicative_instances_for/
-- Dan Burton
On Fri, Aug 16, 2013 at 7:52 AM, Brandon Allbery wrote:
> On Fri, Aug 16, 2013 at
ues as their own one-tuples.
I imagine you could write some fancy hack that uses the type system to
automatically promote values to Oneples of the given value when an
"expected: Oneple Foo, actual: Foo" error occurs. But this would not be
very useful in general.
An uglier option:
type Onep
This is already a separate extension: PatternSignatures. However, that
extension is deprecated for some reason.
On Tue, Aug 6, 2013 at 2:46 PM, Evan Laforge wrote:
> Occasionally I have to explicitly add a type annotation, either for
> clarity or to help choose a typeclass instance. Usually to
ry of Hask. However, it is convenient to have
both in scope unqualified, so maybe lift would not be the best choice.
-- Dan Burton
On Aug 6, 2013 7:38 AM, "Tom Ellis" <
tom-lists-haskell-cafe-2...@jaguarpaw.co.uk> wrote:
> On Tue, Aug 06, 2013 at 04:26:05PM +0200, Jerzy Karczm
let Just x | b = Just 1
where b = x > 0
let Just x | b = Just 1
b = x > 0
These all behave the same way now. Which ones should change?
If Haskell had a non-recursive let, that'd probably be a different story.
But it doesn't.
On Tue, Jul 9, 2013 at 1:
The definition
Just x | x > 0 = Just 1
is recursive. It conditionally defines Just x as Just 1 when x > 0 (and as
bottom otherwise). So it must know the result before it can test the guard,
but it cannot know the result until the guard is tested. Consider an
augmented definition:
Just x
>
> I am not trying to say "every building is a shelter", rather "anything
> that is a building must provide sheltering services".
Well if it walks like a shelter and quacks like a shelter... /shrug
The "is a" relationship is not a good way to think about type classes, in
my opinion. The "interf
There is a package that implements an Int that throws an exception on
overflow:
http://hackage.haskell.org/package/safeint
Since Int's existence is pretty much all about trading for performance, I
wouldn't recommend holding your breath on the above becoming the default.
If you want things to
maybe this will help?
Haskell code in and of itself isn't special. proofs can happen with the
type system, but typically you'd want to define a target language and do
assertions about it, similar to how a compiler inspects it's input
programs. Haskell is not homoiconic nor is it like coq or prolog
i don't understand what you're trying to do with that code, however you
seem to be asking about theorem proving in general
check out
http://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers
and
http://en.wikipedia.org/wiki/Automated_theorem_proving
hope it helps
On Wed, May 1
(oops, forgot to reply all)
if you're on the jvm already why not consider clojure?
it lacks static typing, but S expressions can stand in for haskell types
if you really need them to.
otherwise you'll have to do some fancy JNI calls and worry about calling
haskell from C, like this
http://www.
On Monday 06 May 2013 14:34:13 Tobias Dammers wrote:
> The problem is that people tend to (truthfully) check such a box, then
> stop maintaining the package for whatever reasons, and never bother
> unchecking the box.
I think there should be just one mail per maintainer mail address, not per
pack
lement this with sensible
> characteristics
> > > within the fusion framework.
> > >
> >
> > If you could "solve" concat, might that also lead to be being able to do
> > without the Skip constructor?
>
> Dan is right, we still need Skip. My suggested
really think they're worth saving in general, though. I haven't
missed them, at least.
-- Dan
On Thu, Apr 25, 2013 at 3:19 PM, Gábor Lehel wrote:
> Good point, again. Is that the only problem with it?
>
>
> On Thu, Apr 25, 2013 at 5:57 PM, Dan Doel wrote:
>
>> It
It is not completely backwards compatible, because (for instance) the
declaration:
newtype C a => Foo a = Foo a
was allowed, but:
newtype Foo a where
Foo :: C a => a -> Foo a
is an illegal definition. It can only be translated to a non-newtype data
declaration, which changes the s
like:
Yield 1, Yield 2, Yield 3, Skip, Yield 4, Yield 5, Skip, Skip, Yield 6,
Yield 7, Skip, Done
-- Dan
On Wed, Apr 24, 2013 at 6:52 PM, Gábor Lehel wrote:
>
>
> On Wed, Apr 24, 2013 at 7:56 PM, Bryan O'Sullivan wrote:
>
>> On Wed, Apr 24, 2013 at 10:47 AM, Duncan
Hi all,
I've discovered the excellent proxy library recently and one thing strikes
me. How do you unit test a proxy? Are there any specific methods or
workflows for doing this cleanly and consistently?
Daniel
--
~~ Whatever happens, the sun's still gonna come up tomorrow ~~
Do note that deepSeq alone won't (I think) change anything in your
current code. bug will deepSeq the file contents. And the cons will
seq bug. But nothing is evaluating the cons. And further, the cons
isn't seqing the tail, so none of that will collapse, either. So the
file descriptors will still
ne.
As an aside, you should never use hClose when doing lazy I/O. That's
kind of like solving the above, "i've allocated too much memory,"
problem with, "just overwrite some expensive stuff with some other
cheap stuff to free up space."
-- Dan
On Sun, Mar 17, 2013 a
Just because you can't use the 'magic primitive' in question to
produce an element of the empty type doesn't mean the system is sound
(nor does type soundness have anything to do with proving 'false').
The question is what the primitive is supposed to do. If it's supposed
to work as a witness of e
do block ending in a return
>
> Even that last one is slightly questionable, I feel, but probably works
> for almost all cases. Are there any others?
>
> On Mon, Mar 04, 2013 at 12:20:12PM -0500, Dan Doel wrote:
>> I hadn't seen this before, but I tried it out, and the p
ion mode I use frequently outdents when I type '=>' (which
annoys the hell out of me, because it's almost never correct), but I don't
know if it can be done intelligently enough to be useful (which would be
important). Something to keep in mind, though.
-- Dan
On Sun, Mar
Why not
just write code that writes out the path you want to take and link against
it?
- Dan C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
least the next few weeks. I can promise to occasionally
throw my opinion around as if it mattered, though. ;)
-- Dan Burton
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Sounds great. Lambdabot is an important icon to the Haskell community; it
will be nice to brush off the bitrot and make lambdabot easier for the
average Haskeller to install without having to rely on Cale keeping it
running on irc (grateful, though we are).
-- Dan Burton
On Feb 17, 2013 3:04 PM
system at compile time.
E.g., a Darwin and Win32 modules that provide a function that calls
'SSL.contextSetVerificationMode ctx SSL.VerifyNone', and some kind of
Generic module that provides a function that does the rest.
- Dan C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
with a higher-rank type (whether because it inferred it
separately, or you gave it), and that does trigger the alternate code path.
If that's still too vague, you'll have to refer to the paper.
-- Dan
*
http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidei
On Wed, Jan 2, 2013 at 11:20 AM, Dan Doel wrote:
> Note that even left-to-right behavior covers all cases, as you might have:
>
> f x y
>
> such that y requires x to be checked polymorphically in the same way.
> There are algorithms that can get this right in general,
Your example doesn't work for the same reason the following doesn't work:
id runST ()
It requires the inferencer to instantiate certain variables of id's type to
polymorphic types based on runST (or flip's based on one), and then use
that information to check (id in your example) as a
polymo
s too powerful, nor *how
*that would lead to extensive abuse. Well, "too powerful" or not,
meta-programming should be more easily available at least at *some *layer
of language development without having to resort to hacking the compiler.
-- Dan Burton
___
from the
flexibility proffered to the rest of the language.
tl;dr give me easily extensible syntax, rather than having to run to GHC
devs every time I want a new or different flavor of sugar.
-- Dan Burton
___
Haskell-Cafe mailing list
Haskell-Cafe
Lists! The finite kind.
This could mean Seq for instance.
On Nov 30, 2012 9:53 AM, "Brent Yorgey" wrote:
> On Fri, Nov 30, 2012 at 02:33:54AM +0100, Ben Franksen wrote:
> > Brent Yorgey wrote:
> > > On Thu, Nov 29, 2012 at 03:52:58AM +0100, Ben Franksen wrote:
> > >> Tony Morris wrote:
> > >> >
7;ll add the VS
option next time we run it (I assume they are a small number (?) )
--- On Sat, 11/24/12, Malcolm Wallace wrote:
From: Malcolm Wallace
Subject: Re: [Haskell-cafe] Survey: What are the more common Haskell IDEs in
use ?
To: "Dan"
Cc: haskell-cafe@haskell.org
Date: Saturday
Yes Janek,
I will post the results in a few days/one week max, once we get enough data in.
Dan
--- On Sat, 11/24/12, Janek S. wrote:
From: Janek S.
Subject: Re: [Haskell-cafe] Survey: What are the more common Haskell IDEs in
use ?
To: haskell-cafe@haskell.org
Cc: "Dan"
Date
Because I see there are many preferences on what IDE to use for Haskell
I've created a quick survey on this topic.
Please click here and select your choices from the lists.
http://kwiksurveys.com/s.asp?sid=oqr42h4jc8h0nbc53652
Any comments/suggestions are welcome.
(if any is missing, etc)
Apo
log/2012/11/solving-cabal-hell
-- Dan Burton (801-513-1596)
On Tue, Nov 13, 2012 at 9:27 AM, Andreas Abel wrote:
> After 2 days of shrinking 251 modules of source code to a few lines I
> realized that modify in MonadState causes <> in mtl-2.1.
>
>
> http://hackage.haskell.or
ion. This
is true in category theory, when you talk about algebraic theories,
and it's true in Haskell when you start noticing that various little
languages are described by algebraic theories. But from this angle, I
see no reason why it's _better_ to split variable
n disguise. (And, amusingly, we're even using
polymorphic recursion, so if this isn't in a class, or given an
explicit type signature, inference will silently get the wrong
answer.)
So, there are good reasons for making (>>=) primitive, and not really
any (that I can see) for makin
This is a regression of some sort since the library operates fine within
GHCi for previous versions of GHC. I don't know whether it is a problem
with GHCi, the OpenGL library, or some third party. This is the error
encountered when a module that uses OpenGL tries to load:
Prelude Main> main
Loadin
re (map g xs f = xs (f . g) ; map h (map g xs) = \f -> xs (f . g .
h)).
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
A a c -> A a c
consA x xs = Roll $ \k -> k x xs
-- nilB :: B a c
nilB _ _ = nil
-- consB :: b -> B a c -> B a c
consB y ys x xs = f x y `cons` unroll xs ys
snip
This traverses each list only once.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
t paper (that's
impossible). But parametricity can be used to prove statements _about_
the encodings that imply the induction principle.
> On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel wrote:
>>
>> This paper:
>>
>> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=1
paper above, which
I was pointed to recently).
-- Dan
On Tue, Sep 18, 2012 at 5:41 PM, Ryan Ingram wrote:
> Oleg, do you have any references for the extension of lambda-encoding of
> data into dependently typed systems?
>
> In particular, consider Nat:
>
> nat_elim :: forall P
ith a
constraint 'Foo Int a' which it _won't_ use to determine that a ~
Float.
This is not inherent to fundeps. One could make a version of fundeps
that has the local constraint rules (easily so by translating to the
new type families stuff). But, the difference is also the
us know how it goes!
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
import BasicPrelude
-- Dan Burton
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
small, it can also serve
as a simple demonstration of how to use a cabal flag
in conjunction with CPP to selectively include swaths of code
(see Control/Monad/Tardis.hs and tardis.cabal).
I'm not entirely sold on the naming conventions for the package (including
the package name),
and am open t
>
>
>>> I don't know if it is possible to add haddock to functions whose type
>>> signatures are generated by template haskell.
>>>
>>
>> Could the documentation be an argument of mkLenses?
>>
>
> Does haddock run on the template-haskell expanded code?
TH macros must have type Q [Dec]. Dec has no
e the
lens definitions. Type inference should correctly determine the type of the
generated lenses, but I have structured the library code so that in the
future, type signatures can also be generated. Patches welcome!
http://hackage.haskell.org/package/lens-family-th
-- Dan B
a = 1, b = 1},Foo {a = 2, b = 2},Foo {a = 3, b = 3},Foo {a =
4, b = 4}]
The data seems to pop out of nowhere. Even if Ord instances like the one
for Foo shouldn't exist, they almost certainly will anyways, because the
Haskell type system doesn't prevent them. Users of the library should be
t's a reasonable
thing to do, I might as well try that. I have already started checking out
the larger Haskell projects.
On Thu, Apr 12, 2012 at 12:04 PM, Jeremy O'Donoghue <
jeremy.odonog...@gmail.com> wrote:
> Hi Dan,
>
> I am the maintainer of wxHaskell, but please don&
Hello,
I am a second year computer science student who is very interested in
working on a haskell open source project. I have no particular focus on a
certain type of application. I am open to ideas and to exploring new
fields. What kind of project should I look for considering that I am a
beginn
places for metaprogramming, or perhaps even a type of
algorithms that can be distinguished by means other than the functions
they compute. But to say that functions are that type is false, and
that functions should mean that is, I think, wrong headed.
-- Dan
__
allowed to throw away the components for such a product,
because given a homomorphism f that maps everything to a0, pi_B .
maps everything to b0, regardless of what g is.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
this is that you can easily build up a product that
is a bunch of thunks and cause a stack overflow; I _think_ that's more
of a concern than doing the same with a function. So in practice it
might be harder to do without seq on tuples.
-- Dan
On Wed, Feb 15, 2012 at 9:51 PM, Thomas Schilling
wrote:
> On 15 February 2012 16:17, Dan Maftei wrote:
> >
> > 1 When profiling my code with -auto-all, my .prof file names some
> sub-expressions with a backslash. Cf. below. What are these?
> >
> >
>
> 1 When profiling my code with -auto-all, my .prof file names some
sub-expressions with a backslash. Cf. below. What are these?
e_step
e_step.ewords
e_step.\
e_step.\.\
e_step.update_counts
e_step.fwords
My e_step function binds seven expressions inside a
On Thu, Jan 19, 2012 at 11:11 PM, Dan Doel wrote:
> No, this is not correct. Unfailable patterns were specified in Haskell
> 1.4 (or, they were called "failure-free" there; they likely existed
> earlier, too, but I'll leave the research to people who are
> interest
t;failure-free" there; they likely existed
earlier, too, but I'll leave the research to people who are
interested). They were "new" in the sense that they were introduced
only for the purposes of desugaring do/comprehensions, whereas
refutable vs. irrefutable patterns need to be
A is a retract of B.
http://nlab.mathforge.org/nlab/show/retract
g is the section, f is the rectraction. You seem to have it already.
The definition needn't be biased toward one of the functions.
On Thu, Jan 19, 2012 at 4:24 PM, Sean Leather wrote:
> I have two types A and B, and I want to
uff that shows up on stdout/stderr typically is something we
care about, so it's sensible to include that. If you don't care what
happens there, go ahead and use Debug.Trace. It's pure/referentially
transparent modulo stuff you don't care about.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
On Sun, Dec 25, 2011 at 12:14 AM, Eugene Kirpichov wrote:
> On Sat, Dec 24, 2011 at 10:49 PM, Dan Doel wrote:
>> I think it's good to be clear on all these specifics, and people could
>> do with a better recognition of the difference between (non-)strict
>> and (lazy)ea
azy)eager (hint: you can have an eager, non-strict language).
But it isn't necessarily a problem that people speak in terms of more
than one at once. The different kinds of semantics aren't in conflict
with one another.
The main problem would be that such casual mixing
then you in fact get induction principles based on those models
(see for instance, Fibrational Induction Rules for Initial Algebras).
You need to prove two or three additional cases, but it works roughly
the same as the plain ol' induction you seem to lose for having
non-strict evaluation.
And th
Thank you very much for your answers.
Felipe's suggestion to use waitForProcess after terminateProcess did the
trick. No more zombies around :)
Best regards,
Dan Rosén
On Wed, Dec 7, 2011 at 4:39 PM, Donn Cave wrote:
> Quoth Felipe Almeida Lessa ,
> > On Wed, Dec 7, 2011 at 1:
x27;d
cascade into some thorny issues.
Hopefully that covers all the other subsequent stuff folks have been
talking about.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
, but the timeout resolution is in seconds (same with
eprover's flag --cpu-limit). Any ideas how I could write my code to get a
clean termination of this process?
Best,
Dan Rosén
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.h
o me after a little
thought), and thought I'd float the idea out to the GHC developers, in
case they're interested in picking it up.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
anyone's looking for
motivation, ask yourself if you've ever found let or where useful. And
of course, in this case, we can't just beta reduce the desugared
expression, because of the types involved.
Comprehensions are rather like an expression with a where:
[ x*x + y*y + z*z |
rrays of
variable-length (O(1) lookup)
strings. To this end, there is a (strict) ByteString instance
for the relevant class,
and possibly more such instances to come.
Bug reports, patches, requests, etc. can be sent to me at this address.
Enjoy,
-
way to
specify what type certain variables are instantiated to, but it's sort
of understandable that there isn't, because it'd be difficult to do in
a totally satisfactory way.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
of types, not a function that
computes. So it would be impossible for CPUFunc a = CPUFunc b unless a
= b.
Also, if you have a class whose only content is an associated type,
there's really no need for the class at all. It desugars into:
type family CPUFunc a :: *
ine. You'll see O(1) space usage, but
your time usage has a c*k*n term simply from being expressed by a
composition pipeline, where c is the cost of the unnecessary boxing.
Fusion eliminates this term.
-- Dan
___
Haskell-Cafe mailing list
Haskel
lazy for
efficiency, even if you aren't obligated to do it to determine whether
your optimizations are semantics-preserving.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
sier with
Haskell/GHC. Features like this would be pretty killer to have for
Haskell development; then I wouldn't have to prototype in Agda. :)
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
-> Iterator i o (forall m :: (* -> *). m) a
> -> Iterator i o (forall m :: (* -> *). m) a
>
> Is impredicative polymorphism restricted to the kind *?
The problem is that (forall (m :: * -> *). m) is not a valid type, and forall
is not a valid way to
ce.
However, another option is probably:
[i] -> (forall m. Iterator i o m a) -> (forall m. Iterator i o m a)
which will still have the 'this is impossible' case. You know that the
incoming iterator can't take advantage of what m is, though, so it will be
impossible.
-- Dan
_
ation we want. I think this article is
relevant:
http://existentialtype.wordpress.com/2011/03/15/boolean-blindness/
Inasmuch as we shouldn't be throwing away all propositional information by
crushing to a boolean, we also shouldn't be throwing away information that we
will
sing above, but I don't know the
categorical analogues off the top of my head. Searching for 'closed monoidal'
or 'symmetric monoidal closed' along with linear logic may be fruitful,
though.
-- Dan
___
Haskell-Cafe mailing lis
ght
extensions enabled). ATS would easily be a nicer language in that respect,
though.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
one. Indeed,
I would argue that this is far more important than any hypothetical
per-file licensing.
--
Dan Knapp
"An infallible method of conciliating a tiger is to allow oneself to
be devoured." (Konrad Adenauer)
___
Haskell-Cafe mailing
eption: *** Exception: foo
Actually compiling seems to remove the difference in 7.0.1, at least, because
the output is always:
Foo: foo
regardless of ($) or not ('fix error' hangs without output as well, which
isn't what I thought would happen).
Anyhow, that rules out most general-purpose optimizations (including
strictness analysis, I thought).
- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
sition that those types aren't reducible. For instance, maybe we
have:
data T (f : Nat -> Nat) : Set where
whatever : T f
Without eta, the types aren't equal, so this results in a type error.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
that you can write
functions on that Agda type that would have no corresponding implementation in
Haskell is kind of irrelevant.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
is one reason I posted here. Is
there some other way I should contact them?
I will talk to dcoutts, and see what the current status of the
distributed-operation code is and figure out how much time I can
devote to helping with that.
--
Dan Knapp
"An infallible meth
e
happy just knowing I'd given something back to the Haskell community,
which has given a lot to me.
--
Dan Knapp
"An infallible method of conciliating a tiger is to allow oneself to
be devoured." (Konrad Adenauer)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
F[x] has an A-indexed family of projections:
proj a : (Π x:A. F[x]) -> F[a]
The A-indexed sum Σ x:A. F[x] has an A-indexed family of injections:
in a : F[a] -> (Σ x:A. F[x])
Which are visibly generalizations of the definitions of (co)products you'd
encounter modelling non-dependently t
n Closed Categories
Locally Cartesian Closed Categories and Type Theory
but I can't say that any one paper made everything snap into place. More that
reading quite a few gradually soaked in. And I still feel rather hazy on the
subject.
Hope that helps some.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
t the Church-Turing axiom.
I have no problem with serialize :: (Nat -> Nat) -> IO Nat. The problem is
with (Nat -> Nat) -> Nat. The former can respect the quotient in question via
IO hand waving. Perhaps this distinction is frivolous, but it seems wrong to
make the language in general a
> oh yeah.
>
> serialize :: (a -> b) -> IO String
>
> I still don't really get what we're arguing about.
I don't know.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
1 - 100 of 918 matches
Mail list logo
