Re: Untouchable type variables

[wren romano]

On Thu, May 4, 2017 at 10:20 AM, Wolfgang Jeltsch
 wrote:
> Today I encountered for the first time the notion of an “untouchable”
> type variable. I have no clue what this is supposed to mean.

Fwiw, "untouchable" variables come from existential quantification
(since the variable must be held abstract so that it doesn't escape).
More often we see these errors when using GADTs and TypeFamilies,
since both of those often have existentials hiding under the hood in
how they deal with indices.


> A minimal
> example that exposes my problem is the following:
>
>> {-# LANGUAGE Rank2Types, TypeFamilies #-}
>>
>> import GHC.Exts (Constraint)
>>
>> type family F a b :: Constraint
>>
>> data T b c = T
>>
>> f :: (forall b . F a b => T b c) -> a
>> f _ = undefined

FWIW, the error comes specifically from the fact that @F@ is a family.
If you use a plain old type class, or if you use a type alias (via
-XConstraintKinds) then it typechecks just fine. So it's something
about how the arguments to @F@ are indices rather than parameters.

I have a few guesses about why the families don't work here, but I'm
not finding any of them particularly convincing. Really, imo, @c@
should be held abstract within the type of the argument, since it's
universally quantified from outside. Whatever @F a b@ evaluates to
can't possibly have an impact on @c@[1]. I'd file a bug report. If
it's just an implementation defect, then the GHC devs will want to
know. And if there's actually a type theoretic reason I missed, it'd
be good to have that documented somewhere.

[1] For three reasons combined: (1) @F a b@ can't see @c@, so the only
effect evaluating @F a b@ could possibly have on @c@ is to communicate
via some side channel, of which I only see two: (2) the @(a,c)@ from
outside are quantified parametrically, thus nothing from the outside
scope could cause information to flow from @a@ to @c@, (3) the @T@ is
parametric in @(b,c)@ (since it is not a GADT) so it can't cause
information to flow from @b@ to @c@.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: type error formatting

[wren romano]

On Fri, Oct 23, 2015 at 10:48 PM, Evan Laforge  wrote:
> Here's a typical simple type error from GHC:
>
> [...]
>
> I've been having more trouble than usual reading GHC's errors, and I finally
> spent some time to think about it.  The problem is that this new "relevant
> bindings include" section gets in between the expected and actual types (I
> still don't like that wording but I've gotten used to it), which is the most
> critical part, and the location context, which is second most critical.


+1 to reordering the presentation and to adding bullets (or whatever)
to better demarcate the sections.

I've been bit by this a lot recently. With "normal" type errors it's
quick and easy to figure out what went wrong, but especially when the
issue has to do with type equality constraints, it takes far too much
time to sift through the error message to find the relevant
information[1].

I also wonder whether we should add in some flags for controlling how
much verbosity we get from error/warning messages. Sometimes we want
all the info we can get, whereas other times it'd be nice to just get
the bare minimum (e.g., when we're mainly interested in a yes/no
response and a line number for where things broke)


[1] perhaps type equality errors should be presented differently than
other type errors? The most relevant bits here are (a) what equality
do we need, (b) what equalities do we have, and (c) what are the local
bindings and their types (so we know where the various indices came
from). Which is a bit different from the relevant information for an
"expected Foo, found Bar" type error

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] The evil GADTs extension in ghci 7.8.4 (maybe in other versions too?)

[wren romano]

On Thu, Jun 4, 2015 at 11:43 PM, Edward Z. Yang ezy...@mit.edu wrote:
 GHC used to always generalize let-bindings, but our experience
 with GADTs lead us to decide that let should not be generalized
 with GADTs.  So, it's not like we /wanted/ MonoLocalBinds, but
 that having them makes the GADT machinery simpler.

 This blog post gives more details on the matter:
 https://ghc.haskell.org/trac/ghc/blog/LetGeneralisationInGhc7

The fact that -XGADTs (in isolation) implies -XMonoLocalBinds isn't
the problem. The problem is, the order in which language pragma are
offered should not matter. Whether I say {-# LANGUAGE GADTs,
NoMonoLocalBinds #-} or {-# LANGUAGE NoMonoLocalBinds, GADTs #-}
shouldn't matter. Both should mean the same thing, regardless of how
annoying it may be to work in that language.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] RFC: Native -XCPP Proposal

[wren romano]

On Fri, May 8, 2015 at 12:12 PM, Dan Doel dan.d...@gmail.com wrote:
 vector generates a considerable amount of code using CPP macros.

 And with regard to other mails, I'm not too eager (personally) to port that
 to template Haskell, even though I'm no fan of CPP. The code generation
 being done is so dumb that CPP is pretty much perfect for it, and TH would
 probably just be more work (and it's certainly more work to write it again
 now that it's already written).

Incidentally, if we really want to pursue the get rid of CPP by
building it into the GHC distro...

In recent years there've been a number of papers on variational
lambda-calculi[1] which essentially serve to embed flag-based
preprocessor conditionals directly into the language itself. One major
benefit of this approach is that the compiler can then typecheck *all*
variations of the code, rather than only checking whichever particular
variation we happen to be compiling at the time. This is extremely
useful for avoiding bitrot in the preprocessor conditionals.

...If we were to try and obviate the dependency on CPP, variational
typing seems like a far more solid approach than simply reinventing
the preprocessing wheel yet again. (The downside, of course, is making
the Haskell spec significantly more complex.)


[1] e.g., http://dl.acm.org/citation.cfm?doid=2398856.2364535

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: [Haskell-cafe] RFC: Native -XCPP Proposal

[wren romano]

On Wed, May 6, 2015 at 9:05 AM, Alan  Kim Zimmerman
alan.z...@gmail.com wrote:
 Perhaps it makes sense to scan hackage to find all the different CPP idioms
 that are actually used in Haskell code, if it is a small/well-defined set it
 may be worth writing a simple custom preprocessor.

Conditional imports are far and away the most commonly used idiom.
Second most common, I'd say, is specifying GHC-specific vs
compiler-generic implementations of top-level functions (e.g., using
GHC.Exts.build or not). For both of these it's sufficient to have the
#if construction plus everything needed for the conditional
expressions.

However, while the #if construction covers the vast majority of use
cases, it doesn't cover all of them. Macros are also important. For
example, a number of low-level libraries will use macros for things
like having assertions which are either compiled as runtime checks, or
as nothing, depending on a Cabal flag. Of course, there are plenty of
other places where we want to use macros in low-level code, either to
force inlining, or to have conditional compilation of (non-top-level)
expressions that show up over and over. That these idioms aren't more
common is just because there aren't more people working on such
low-level code.

In theory TH should be able to handle this stuff, but TH is a verbose
sledgehammer for these sorts of problems, and using TH means
restricting yourself to being GHC-only.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Re: Avoiding BlockedIndefinitelyOnSTM exceptions

[wren romano]

On Sun, Jul 20, 2014 at 5:22 PM, Gábor Lehel glaebho...@gmail.com wrote:
 On Sun, Jul 20, 2014 at 5:48 AM, wren romano winterkonin...@gmail.com
 wrote:

 On Sat, Jul 19, 2014 at 11:24 PM, wren romano winterkonin...@gmail.com
 wrote:
  -- | The second argument allows handling 'BlockedIndefinitelyOnSTM'
  etc.
  runSTSTM :: (forall s. STSTM s a) - (STMError - b) - b

 That should've been something more sensible, like:

 atomicallySTSTM :: (forall s. STSTM s a) - (STMError - b) - IO
 (Either a b)

Yeah, that's not quite what I meant either. Will have to think about it more.

 Wouldn't combining it wih ST defeat the purpose of STM? The purpose of STM
 being to synchronize access to shared variables using atomic transactions.
 If all the variables in your atomic transaction are guaranteed to be local
 and not touched by any other transaction, which I believe the above type
 says, then you don't need a transaction at all.

 Or was the idea to create some kind of outer scope within which individual
 atomic (sub)transactions may share access to variables, but not without?

Yeah, the idea is to create smaller scopes to collect all the related
references into a single heap/region, isolating them from other heaps,
allowing the heap to be gc'ed in one go, etc. Arranging local scopes
is generally a good idea since global scope is non-compositional.

STM just says that heap interactions are transactional, it doesn't say
there can be only one heap/region. Indeed, there can be performance
benefits for adding regions to thread-based parallelism like STM.
Since threads accessing disjoint regions cannot interfere with one
another we have very strong guarantees about their data-flow and
synchronization properties. This, in turn, can be used by the runtime
to reduce memory traffic: associate each heap with a core, distributed
as evenly as possible over the cores, and schedule all the threads
over a given heap to be run on the core for that heap (or on nearby
cores). Similarly there can be runtime performance benefits since we
can use tricks like card marking to quickly check whether any other
thread has modified our region; if not, then commit immediately; if
so, then do the expensive check of running through the STM log to see
if there's really a conflict.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Avoiding BlockedIndefinitelyOnSTM exceptions

[wren romano]

On Mon, Jul 14, 2014 at 11:16 AM, Gabriel Gonzalez gabriel...@gmail.com wrote:
 I don't quite understand your question, but I'll try to give a fuller
 explanation of the problem I was trying to solve to see if it perhaps
 answers your question.

I think the suggestion was something like this:

-- | The @s@ type is an abstract heap id just like in 'ST'.
type STSTM s a

-- | The second argument allows handling 'BlockedIndefinitelyOnSTM' etc.
runSTSTM :: (forall s. STSTM s a) - (STMError - b) - b

The idea being that, if the problem with catching
BlockedIndefinitelyOnSTM has to do with the fact that all STM
variables have global scope and so even if we could catch the
exception itself we'd still have problems with cleaning up the
collateral damage[1], then that's why it doesn't make sense to allow
BlockedIndefinitelyOnSTM to be caught. However, by using an abstract
heap-id we can bundle all related STSTM variables together, and we
know that once runSTSTM exits they can't be accessed from anywhere
else— so even if there's an error, we can still clean up all the
variables, threads, and other jetsam associated with this STSTM
computation.

[1] I don't know if this is actually the reason why why
BlockedIndefinitelyOnSTM is uncatchable, rather it sounded like this
is what Neil Davies was suggesting to be the reason. Also, I do seem
to recall something like this actually being the case; though it's
unclear whether the STSTM approach would actually be able to solve the
problem.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Avoiding BlockedIndefinitelyOnSTM exceptions

[wren romano]

On Sat, Jul 19, 2014 at 11:24 PM, wren romano winterkonin...@gmail.com wrote:
 -- | The second argument allows handling 'BlockedIndefinitelyOnSTM' etc.
 runSTSTM :: (forall s. STSTM s a) - (STMError - b) - b

That should've been something more sensible, like:

atomicallySTSTM :: (forall s. STSTM s a) - (STMError - b) - IO
(Either a b)

 The idea being that, if the problem with catching
 BlockedIndefinitelyOnSTM has to do with the fact that all STM
 variables have global scope and so even if we could catch the
 exception itself we'd still have problems with cleaning up the
 collateral damage[1], then that's why it doesn't make sense to allow
 BlockedIndefinitelyOnSTM to be caught.

 [1] I don't know if this is actually the reason why why
 BlockedIndefinitelyOnSTM is uncatchable, rather it sounded like this
 is what Neil Davies was suggesting to be the reason. Also, I do seem
 to recall something like this actually being the case; though it's
 unclear whether the STSTM approach would actually be able to solve the
 problem.

Fwiw, after (re)reading ezyang's blog post about
BlockedIndefinitelyOnSTM, it seems clear that this is not actually
what the problem is. Though he also mentioned that the exact details
of BlockedIndefinitelyOnSTM shouldn't be relied upon, since the
exception is just a trick to kill off useless threads in order to
collect more garbage.

...

In terms of solving your actual problem in pipes, it seems like what
you really want are weak-references for STM. That way you don't rely
on the behavior of BlockedIndefinitelyOnSTM, and you can still get
garbage collection to send you signals whenever something becomes
inaccessible, allowing you to handle things however you like. Seems
like it shouldn't be too hard to do, since weak-references for IO are
already supported; though, of course, it'll still take a fair deal of
hacking to implement it.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Bang Patterns

[wren romano]

On Tue, Apr 1, 2014 at 3:02 PM, Dan Doel dan.d...@gmail.com wrote:
 Specifically, consider:

 case Nothing of
   !(~(Just x)) - 5
   Nothing - 12

 Now, the way I'd expect this to work, and how I think the spec says it
 works, is that my Nothing is evaluated, and then the irrefutable ~(Just x)
 matches Nothing, giving a result of 5. In fact, GHC warns about overlapping
 patterns for this.

It's sensible to give an overlap warning --that is, assuming we don't
want overlap to be an error-- since the irrefutable pattern matches
everything, and adding bangs doesn't change what values are matched
(it only changes whether we diverge or not).

However, I have no idea how top-level bang in case-expressions is
supposed to be interpreted. If anything, it should be ignored since we
must already force the scrutinee to WHNF before matching *any* of the
clauses of a case-expression. However, I thought bangs were restricted
to (1) immediately before variables, and (2) for top-level use in
let/where clauses...

In any case, following the standard desugaring of the specs:

case Nothing of !(~(Just x)) - 5 ; Nothing - 12

=== { next to last box of
http://www.haskell.org/ghc/docs/latest/html/users_guide/bang-patterns.html,
the proposed clause (t) for section 3.17.3, figure 4 }

Nothing `seq` case Nothing of ~(Just x) - 5 ; Nothing - 12

=== { Haskell Report, section 3.17.3, figure 3, clause (d) }

Nothing `seq` (\x - 5) (case Nothing of Just x - x)

Which most definitely does not evaluate to 12. Either the specs are
wrong (dubious) or the implementation is. File a bug report.

-- 
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users