- Haskell-Cafe - Haskell.org

Type constraint rewrite rules
by Henning Thielemann 22 Jan '23

22 Jan '23

Has anyone thought about rewrite rules for type constraints as light-weight alternative to type-checker plugins? Rewrite rules could be n + 'Zero -> n Back (Forth a) -> a for closed type families Back and Forth, where Back is the inverse of Forth Ideally the programmer would also provide a correctness proof for the proposed rewrite, e.g. with a function that generates a data BackForthProof a = (Back (Forth a) ~ a) => BackForthProof

2 1

Foldable intercalate for Data.Text?
by Benjamin Redelings 21 Jan '23

21 Jan '23

Hi, I was looking at intercalate in Data.Text, and I see that the signature is Text -> [Text] -> Text. I'm curious why this isn't (say) Foldable f => Text -> f Text -> Text Perhaps because this would be harder to optimize? -BenRI

2 2

Anyone working on improving HPC
by Ivan Perez 21 Jan '23

21 Jan '23

Hi everyone, A while back there were a few exchanges about the state of HPC and I remember reading that someone was interested in pushing a bit for improving the tool and the reports generated. Does anyone know if that's happening and who is working on that? I forgot where I saw it and I can't find it. It could have been haskell-cafe, discord, chat, idk. Thanks, Ivan

7 6

Everything you never wanted to know about Applicative laws and more
by Alexandre Esteves 21 Jan '23

21 Jan '23

I've spent some time recently going down this particular rabbit hole. The original motivation was replacing the current formulation of Applicative laws with the Monoidal-ish one, but one thing led to the other and I ended up making a post about the various sets of laws and related free theorems: https://github.com/alexfmpe/semantic-satiation/blob/main/src/Posts/001-appl…

1 0

C++ Haskell interpreter with GADTs + Type Families + Rank-n types
by Benjamin Redelings 21 Jan '23

21 Jan '23

Hi all, I don't want to oversell this, but in case anyone is interested, I've been working on a Haskell interpreter that is written in C++. This isn't intended to compete with GHC. It doesn't generate machine code, and it is not fast. However, I had a reason to try and implement Haskell typechecking in C++. So if anyone is interested in how to write their own Haskell compiler, then this might possibly be of interest. Otherwise, probably not. So far I have: 1. Parser 2. Renamer - hacky. Infix handling is a separate pass. 3. Typechecker - standard constraints + rank n types + GADTS + type families. But no newtypes and no coercions. 4. Desugarer - the desugarer generates a language w/o type-level lambdas or coercions. 5. Optimizer - inlining, let-floating, case-of-case, etc. No SpecConstr. No Rules. 6. Translation to de-Bruijn notation prior to execution (See Sestoft 1997, "Deriving a lazy abstract machine") 7. Interpreter - a special-purpose dependency-tracking interpreter. The revelant code is here: https://github.com/bredelings/BAli-Phy/tree/master/src/computation After compiling the executable, you would run use it to run a Haskell program like this: bali-phy --run-module Main.hs Tests are in: https://github.com/bredelings/BAli-Phy/tree/master/tests/haskell -BenRI

2 3

Re: [Haskell-cafe] induction on type-level Nat
by Olaf Klinke 16 Jan '23

16 Jan '23

> Alternative approach with a GADT: > > data T n a where > End :: T 0 a > Cons :: a -> T n a -> T (n+1) a > > viewL :: T (n+1) a -> (a, T n a) > viewL (Cons x xs) = (x, xs) > > testEnd :: T 0 a -> () > testEnd End = () > > > For viewL GHC reports a missing pattern match on 'End' and for > testEnd it > reports a missing match on 'Cons'. If I add the constraint (1<=n+1) > to > Cons then the testEnd warning disappears. If I add the constraint > (1<=n+1) > to viewL, then its warning disappears, as well. So the theory of type-level nats lacks the theorem forall m n. n+m <= n :: Nat -> Nat -> Constraint The infix type operator + from GHC.TypeLits constrains n in Cons to kind Nat. So the theorem above ought to be available to the type checker. Hiromi's type-natural package has Lemmas plusLeqL and plusLeqR for this. Olaf

1 0

Re: [Haskell-cafe] [ANNOUNCE] GHC 9.6.1-alpha1 is now available
by Ben Gamari 16 Jan '23

16 Jan '23

George Colpitts <george.colpitts(a)gmail.com> writes: > Hi > > I believe llvm does not work in this alpha as 21936 is still open. Is that > correct? > Indeed we do not yet support LLVM 15 but all previous LLVM versions continue to work. We can try to fix this for the final release. > I also believe that when it does work it will require llvm 15 which will be > incompatible with earlier versions of ghc. Is that correct? > Early indications suggest that supporting LLVM 15 will require that we raise the minimum supported version to LLVM 13. Cheers, - Ben

1 0

induction on type-level Nat
by Henning Thielemann 16 Jan '23

16 Jan '23

I want to define a list with type-level Nat length: type family List (n::Nat) :: Type -> Type where List 0 = End List n = Cons (List (n-1)) data End a = End data Cons f a = Cons { head :: a, tail :: f a } But this way, GHC cannot match ‘List (n+1)’ with ‘Cons (List n)’, also not with the magic type checker plugings suggested before. I guess I need a another way to define List or some support for the type checker to accept List (n+1) ~ Cons (List n).

1 2

[ANNOUNCE] GHC 9.6.1-alpha1 is now available
by Ben Gamari 13 Jan '23

13 Jan '23

The GHC team is very pleased to announce the availability of GHC 9.6.1-alpha1. As usual, binaries and source distributions are available at downloads.haskell.org: https://downloads.haskell.org/ghc/9.6.1-alpha1/ This is the first alpha release in the 9.6 series which will bring a number of exciting features: * A new Javascript code generation backend * A new WebAssembly code generation backend, * Significant latency improvements in the non-moving garbage collector * Support for loading of multiple components in GHCi * Efficient support for delimited continuations * Improvements in error messages * Numerous improvements in compiler-residency Note that both the Javascript and WebAssembly backends are still in a state of infancy and are present in this release as a technology preview; we hope that they will mature considerably before the final 9.6.1 release. Please give this release a try and open a [ticket] if you see anything amiss. Cheers, - Ben [ticket]: https://gitlab.haskell.org/ghc/ghc/issues/

1 0

Re: [Haskell-cafe] Current state of type-level natural number programming
by Henning Thielemann 13 Jan '23

13 Jan '23

On Fri, 13 Jan 2023, rowan goemans wrote: > I'm a heavy user of ghc-typelits-natnormalise. > > I can feel your pain that it sometimes isn't able to solve seemingly "simple" > constraints. But not all is lost in those cases. The `constraints` package > allows one to solve `Nat` constraints out of thin air, provided you go > through a function to do it. > > nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0) > nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a))) Good to know that there are ways to add missing transformations. Ideally there would be a way without unsafeCoerce, i.e. that I could prove a property manually using some proof steps expressed in functions. Alternatively, maybe I can write missing steps in a custom type checker plugin. Has someone already tried to connect SBV to a type checker plugin?

2 1