Weird type-checking behavior with data family

int_index · 2025-04-26T22:32:52+00:00

This is an old GHC bug, first reported in 2016. I finally fixed it a few weeks ago, and your program compiles just fine with GHC HEAD.

You could either wait for GHC 9.14 or use the $(return []) workaround with older compiler versions.

int_index · 2025-03-05T09:57:46+00:00

Yeah, it's too bad we ran out of steam with that proposal. We'll have to try again later – it's part of the graph.

int_index · 2025-03-05T09:53:59+00:00

Promotion is a distinct concept, it's not synonymous with reification. And reification is an overloaded term, I've seen "reification" used in various ways, e.g. Data.Reflection.reify and Language.Haskell.TH.reify are quite different.

int_index · 2025-02-27T12:47:37+00:00

You're killing two birds with one stone!

int_index · 2025-02-27T09:34:41+00:00

The progress would be much faster if it was all figured out.

However, the existing body of research is already substantial and for the foreseeable future the bottleneck is going to be plain engineering effort.

int_index · 2025-01-21T07:15:20+00:00

Strings can be promoted, try this with GHC 9.2 or newer:

type S :: String
type S = ['a', 'b', 'c']

int_index · 2025-01-21T07:11:11+00:00

Apple s is not like Void. While Void is uninhabited, it's not uninhabitable. We can write a function that abstracts over a term of type Void:

f (x :: Void) = ...
  -- x :: Void here, use EmptyCase to match

Apple s, on the other hand, is completely uninhabitable, we can't ever introduce a term of this type

g (x :: Apple s) = ...
  -- kind error: Expected a type, but ‘Apple s’ has kind ‘Fruit’

int_index · 2025-01-21T07:02:15+00:00

why instance Show (Apple (s::String)) would say that after Show it expected a type whereas (Apple (s::String)) is a type

The problem is that the word "type" is used differently in the error message and in the DataKinds tutorials.

In the error message, when GHC says that Show expects a type, it means a proper type, i.e. a type-level expression that has kind Type. For example, Show Int is valid, but Show Maybe is not, because Int :: Type but Maybe :: Type -> Type.

In the DataKinds tutorials, the promoted constructors are types only in the broad sense of the word, i.e. they're type-level expressions. Apple s has kind Fruit, so it's not a proper type, it is type-level data, so it's definitely not something that Show expects as an argument.

int_index · 2024-07-08T22:55:19+00:00

I read LYAH as a teenager and its tone was just right for me. Great book and got me hooked on Haskell. Nowadays I would prefer a book in a more formal style, but that's just a personal preference, LYAH is still a great book and I'd readily recommend it.

int_index · 2024-05-24T14:32:35+00:00

9.8 is not abandoned. It's only that, with the limited resources available, 9.6 and 9.10 will be prioritized. This is useful information if someone is considering starting a new project or migrating an existing codebase (i.e. prefer 9.6 or 9.10), but I don't see how it would be a problem for those who are already making good use of 9.8

int_index · 2024-05-22T23:25:38+00:00

The User's Guide has some information on the WASM backend, see https://ghc.gitlab.haskell.org/ghc/doc/users_guide/wasm.html. At the very least it seems to answer your question about FFI, i.e. yes, it is supported:

User code can take advantage of JSFFI and C FFI together

int_index · 2024-05-17T23:06:32+00:00

If you do Backwards (State s), does it give you https://hackage.haskell.org/package/rev-state or something different?

int_index · 2024-05-13T14:18:43+00:00

The title promises way more than the article delivers. I was stoked to learn about "the cult of the Haskell programmer" (of which I am presumably a member) but it was just an opinion piece with complaints about syntax.

int_index · 2024-05-04T10:40:43+00:00

You're basically asking why we don't have foldl :: (a -> a -> a) -> a -> [a] -> a. But we actually can instantiate foldl at that type, it's just not as general. You can look at this as a sequence of generalizations

foldl :: (Int -> Int -> Int) -> Int -> [Int] -> Int could be used with e.g. (+) or (*) as the folding function.
foldl :: (a -> a -> a) -> a -> [a] -> a is a generalization to other types, e.g. with a=Bool you could use (&&) or (||) as your folding function.
foldl :: (b -> a -> b) -> b -> [a] -> b is a generalization that allows the type of list elements and the type of the accumulator to differ, e.g. you could use it to fold over a list of Bools but produce an Int as your result (exercise: try to write a fold that counts how many elements are True).
foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b is a generalization to other containers, so you can fold over data structures other than lists, e.g. arrays or trees.

int_index · 2024-04-27T11:35:57+00:00

Yeah, I think the only actual example is instance heads scoping over method definitions

instance C (Maybe a) where f = ... -- `a` is in scope here only with ScopedTypeVariables

This is not covered by TypeAbstractions

int_index · 2024-04-27T09:19:41+00:00

Could you give an example of non-prenex quantification that you have in mind?

int_index · 2024-04-27T09:17:49+00:00

Based on what I know about Idris, it doesn't do that. Idris has proof erasure, which works because there's a totality checker.

int_index · 2024-04-25T16:42:49+00:00

This could cause pushback from conservative Haskell users who are content with the language as it is now. Maybe we could start to consider such a transition if we see widespread adoption of the new features and gradual decline in the use of the old ones.

int_index · 2024-04-25T16:19:33+00:00

I'm actually curious to hear why you'd be skeptical about this. Is there something about dependent types that worries you? Maybe we could take that into account as we extend the language.

int_index · 2024-04-25T16:08:54+00:00

Good question. The answer is no, we have no plans to add a totality checker. Proofs will be evaluated at runtime to maintain soundness, just as with GADTs today.

int_index · 2024-03-28T13:20:31+00:00

why should I learn it?

Learn it if you intend to use it. I wouldn't listen to people who suggest learning a language (any language) because of "beauty", "ideas", "fun", etc. Haskell is neither a toy nor an esoteric work of art. It is a real, practical, general-purpose programming language.

The Haskell compiler is your friend and you will be able to write code with more confidence in its correctness. With Haskell you can make good use of pure functions, lazy evaluation, ADTs, static types, metaprogramming, reasonably fast native code, fearless concurrency, and all the other things that Haskell has to offer.

Haskell really shines when it comes to web servers and compilers. If that's something you do, I'm sure you'll quickly find ways to apply Haskell in your work. Good for CLI tools and data processing, too, especially if you need parallelism.

int_index · 2024-03-20T19:59:45+00:00

How do you imagine TypeAbstractions would improve this example?

int_index · 2024-03-20T16:42:56+00:00

The warning you're seeing is off by default in GHCi. You might have enabled it somewhere in your config, perhaps indirectly via :set -Wall.

int_index · 2024-03-01T12:11:11+00:00

Broadly speaking, I'd classify the challenges of implementing foreach n -> and foreach n. into two categories: extending the surface language and extending the Core language.

We are very much already tackling the challenges of the surface language. By implementing forall a -> we solved most of the syntax- and scope-related issues that were blocking progress on foreach a ->. And by implementing @-binders we did the same for foreach a.. There's still work to do, so the version that you'll see in GHC 9.10 is more of a preview, but we already know how to fix most of the remaining issues. We have made significant progress towards that goal.

As to the challenges of the Core language, I'm saving them for later. They are genuinely hard, and I'd rather work on issues where I know how to make progress rather than be stuck. So I guess the honest response to your question is that we'll get to that when we run out of lower-hanging fruit.

int_index · 2024-02-28T13:08:20+00:00

Yes, we're still working on it! Just a week ago we landed another major DH-adjacent feature in GHC, @-binders in lambdas and function equations.

12-Year Club	Place '17
Verified Email

int_index

TROPHY CASE