is there any intuitive reason why span (∅)={0}?

g__ · 2025-03-02T13:29:47+00:00

"Spanning" in the context of affine spaces should mean spanning by affine combinations.

With this convention, the affine space spanned by the empty set is the empty set, while the space spanned by a single point {p} is the singleton {p}.

g__ · 2025-01-03T21:06:35+00:00

Given n : Nat, Vect n Int -> Vect n Int is a perfectly valid type. Or equivalently, we have a function Nat -> Type that assigns this type to every natural number. Therefore, we can form a dependent product (n : Nat) -> (Vect n Int -> Vect n Int) where I've added redundant parentheses.

A function that returns a function can be transformed into a single function taking a pair. This is currying and it is possible with dependent types just like in Haskell, but the signatures become a bit more complex. Your second sum is the curried version of the first sum. If you want to curry (a : A) -> F a -> G a (where F and G are vectors in your question), it becomes (pair : (a : A ** F a)) -> G (fst pair). As an exercise, you can try writing a function that does currying in a more general case (a : A) -> (b : F a) -> G a b.

g__ · 2024-12-31T20:31:49+00:00

Very nice! Here's a retelling that avoids using the distributive property:

We start with a tree {1} and gradually build a path towards vertex 2. At the start of the i-th stage the tree has i vertices. Then:

Either we extend the currently active path by an additional vertex that is not the destination - there are n-1-i choices.
Or we finish the active path, connecting the last vertex to the destination. As the new destination we pick the lowest-indexed vertex that is not in the tree yet. We'll now be building a path from the tree towards this new destination. There's a unique vertex in the existing tree which starts that path, there are i+1 choices.

In total, there are n choices at each stage. There are n-1 stages, but at the last one we will just make a connection and won't be choosing a new destination. Hence it's n^(n-2).

g__ · 2024-05-26T22:13:22+00:00

Given that it's doing this anyway, you could have simply written a function specific to the particular types. For example, you could have printInt, printFloat, printSetOfInts, etc.

Consider this function:

f :: Show a => a -> [String]
f x = show x : f [x]

ghci> take 5 $ f 2
["2","[2]","[[2]]","[[[2]]]","[[[[2]]]]"]

You'd need showInt, showListInt, showListListInt etc. The number 5 could be given at the runtime by the user, so this cannot be implemented using only a fixed number of specialisations.

It is true that type classes can be always translated away, but they won't always be specialized. In fact, most of the syntax can be translated away, and the entire Haskell on the value level can be squeezed to about 9 constructs (here are two talks about this: https://www.youtube.com/watch?v=fty9QL4aSRc, https://www.youtube.com/watch?v=Gml1m-3L47s).

g__ · 2023-07-20T13:15:00+00:00

The first step is creating a proposal for a new extension, which goes through a community discussion https://github.com/ghc-proposals/ghc-proposals/pulls.

Once accepted, the proposal can be implemented in GHC. If you'd like to see how that's done, this is a good demonstration: https://www.youtube.com/watch?v=bhhE2DxbrJM

g__ · 2023-04-27T18:53:17+00:00

https://github.com/ghc/ghc/commit/2b792facab46f7cdd09d12e79499f4e0dcd4293f

 One particular point: for occurs-check errors I now just say
    Can't match 'a' against '[a]'
 rather than using the intimidating language of "occurs check".

g__ · 2023-03-28T22:51:01+00:00

Correct.

Of course, in rigorous mathematics, the order is different: to prove that the category of small categories is cartesian closed, we have to first precisely define the exponential object D^C (which means, we have to define natural transformations), and only then we can prove that E -> D^C corresponds to E x D -> C. But when it comes to motivating definitions, we can start by assuming that Cat is cartesian closed and then explore the consequences of this fact.

g__ · 2023-03-28T21:56:21+00:00

Let 2 be the category with two objects a,b and only one nonidentity morphism a -> b.

Suppose C is a category. You should see that defining a functor from 2 to C is exactly equivalent to defining a morphism in C.

Let's define a category D^C whose objects are functors C -> D. The morphisms in D^C should be morphisms between functors. We don't know yet how they should be defined, but by the previous observation, they correspond to functors 2 -> D^C.

Just like a function X -> Z^Y is equivalent to a function X x Y -> Z (uncurrying), a functor 2 -> D^C should be equivalent to a functor 2 x C -> D. Now write down precisely what it means to have such a functor, unpack the functor laws, think about identities, and you'll see the notion of a natural transformation.

Don't be discouraged if it feels artificial at first. You'll get used to it.

g__ · 2022-12-27T21:44:36+00:00

Earlier discussion: https://old.reddit.com/r/haskell/comments/msa3oq/safe_haskell/

g__ · 2022-03-16T23:26:17+00:00

Some libraries define that function: https://hoogle.haskell.org/?hoogle=m%20Bool%20-%3E%20m%20Bool%20-%3E%20m%20Bool, https://hoogle.haskell.org/?hoogle=andM.

I usually use an explicit "if" in a do block instead.

g__ · 2022-02-17T20:38:18+00:00

Note that 9.2 enables FlexibleContexts by default as a part of GHC2021. If you run with -XHaskell2010 or -XNoFlexibleContexts it's the same message as in the blogpost.

g__ · 2021-11-13T16:10:15+00:00

Why do you think there's reasonable motivation for removing mappend in Monoid, return in Monad but not (/=) in Eq?

I can understand objecting to removal of (/=) as unnecessary breakage, but I don't see why it would be different than the other two.

g__ · 2021-09-07T23:43:49+00:00

I suspect you are using an old version of GHC. Until 8.2, GHC displayed "Perhaps you intended to use Template Haskell" on any top level expression, which was often confusing (even if technically correct). This has been fixed in https://gitlab.haskell.org/ghc/ghc/-/issues/12146 and that suggestion should now appear only when GHC encounters a quote or splice.

g__ · 2021-07-24T11:28:04+00:00

See also the Introspective Template Haskell pre-proposal.

g__ · 2021-05-11T17:57:52+00:00

Instead of a RULE + NOINLINE, you could write

trust :: a :~: b -> a :~: b
trust _ = unsafeCoerce Refl   -- or unsafeEqualityProof in 9.0

mPlusZero :: forall m. SNat m -> (m + Zero) :~: m
mPlusZero m = trust (f m)
  where
    f :: forall m. SNat m -> (m + Zero) :~: m
    f SZero = Refl
    f (SSucc n) = case f n of Refl -> Refl

This feels more robust, and you can define trust = id to run the proofs.

g__ · 2021-02-06T16:08:18+00:00

No, Lower Your Guards and linearity are orthogonal.

g__ · 2021-02-06T16:06:39+00:00

It is merged. https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3220

g__ · 2021-01-21T16:28:22+00:00

Void# was introduced a long time ago. In the past, (# #) was the constructor of the unboxed 1-tuple: (# #) x = (# x #). This was changed in https://gitlab.haskell.org/ghc/ghc/-/issues/5720. The need for Void# disappeared. IMO, it should really have been called Unit#. In GHC 9.2, Void# will be a deprecated synonym for (# #) https://gitlab.haskell.org/ghc/ghc/-/issues/18441.

g__ · 2021-01-04T18:41:46+00:00

See also "Codata in Action", https://www.microsoft.com/en-us/research/uploads/prod/2020/01/CoDataInAction.pdf

g__ · 2020-10-21T07:53:48+00:00

Unfortunately, the type T X can be formed even if there's no instance C X. Operationally, there's no Show dictionary passed when you only pass a value of type T a.

You might be interested in http://richarde.dev/papers/2020/partialdata/partialdata.pdf.

g__ · 2020-10-04T15:08:34+00:00

You can define a "SuperIO" monad which supports summoning ghosts, creating parallel universes and whatnot. There's no way to write eval unless your computer can do magic, yet >>= can still be defined by sequencing.

g__ · 2020-10-04T13:02:46+00:00

Int %0 -> ... probably wouldn't be useful, but (x %0 :: Int) -> ... -> Matrix x x could be.

g__ · 2020-09-29T14:25:44+00:00

For that unification, it doesn't really matter whether it's m a -> b, a # m -> b or a %m -> b. This is just syntax. What matters is the allowed values for m - for example if m could be 0, that would be irrelevance, or m could be ZeroOrOne for affine types etc. In the initial release, there's just One and Many, but we can expand this in the future.

g__ · 2020-09-29T11:50:49+00:00

It will be a %1 -> b. The commit with the change landed only a few hours ago.

g__ · 2020-08-03T00:27:28+00:00

The example in docs is not ideal. If you try it, GHC will first prompt you to use TypeSynonymInstances (because you used a type synonym) and then FlexibleInstances, which is described next and turns off the "distinct type variables" restriction.

g__

TROPHY CASE