- Haskell-Cafe - Haskell.org

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

Current state of type-level natural number programming
by Henning Thielemann 13 Jan '23

13 Jan '23

Almost ten years ago I tried to convert the package llvm-tf to use type-level naturals but it did not lead very far. What is the current state of type-level natural number programming and reasoning? I need type-level naturals for vectors of static size. The type checker must know things like: n+n ~ 2*n n*m ~ m*n (Pos - positive natural number) n::Nat, m::Pos -> n+m :: Pos n::Nat, m::Pos -> n*m :: Nat n::Pos, m::Pos -> n*m :: Pos I need to access an element from a heterogeneous list with a typenat index. That is, I need a kind of induction. I know of ghc-typelits-natnormalise, but it has some problems with inequalities that I need: "Could not deduce n~0 from the context n<=0" https://github.com/clash-lang/ghc-typelits-natnormalise/issues/33 "Could not deduce: (n0 + 1) ~ m from the context: 1 <= m" https://github.com/clash-lang/ghc-typelits-natnormalise/issues/59 So, what is the current state of the art? What libraries, what GHC extensions? Any tutorials?

5 6

Emily Pillmore presentation on Haskell
by Jonathan Drews 13 Jan '23

13 Jan '23

Hi Folks: Next Tuesday, January 17th, Emily Pillmore will give an online presentation to South Eastern Michigan BSD User group (http://www.semibug.org/) at 7 PM Detroit, MI time. I will post the Jitsi link to this list the day before the meeting. I believe the talk will be about 40 - 60 minutes long. It may cover the following topics: * An overview of the Haskell programming language * The Haskell Foundation: what it does and the resources it offers. * Cabal: Common Architecture for Building Applications and Libraries * Question and answer session. -- Kind regards, Jonathan

1 1

Fully Funded PhD Scholarship at St Andrews
by Christopher Brown 11 Jan '23

11 Jan '23

We have a fully funded PhD scholarship available in the School of Computer Science at the University of St Andrews on "Trustworthy Refactoring Tools for Haskell Programs". Any potential candidates are advised to contact Chris Brown (cmb21(a)st-andrews.ac.uk<mailto:cmb21@st-andrews.ac.uk>) for more information. Full details of the scholarship, the general topic, and how to apply are here: https://blogs.cs.st-andrews.ac.uk/csblog/2023/01/11/fully-funded-phd-schola… The deadline for applications is the 1st March 2023 with a September start-date (although there is room for some flexibility due to circumstances). The scholarship is fully funded for 3.5 years. The positions are open for both UK and international applications. You can apply formally at https://www.st-andrews.ac.uk/computer-science/prospective/pgr/how-to-apply/ Kind regards, Chris

1 0