- Haskell-Cafe - Haskell.org

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

Actual levity polymorphism
by Tom Ellis 11 Jan '23

11 Jan '23

I'm investigating unboxed types in GHC 9.2. Levity polymorphism seems to be severely limited in a way that makes it hard to envisage a Haskell ecosystem which comfortably combines lifted and unlifted types. Am I missing something? Understandably, the following attempt at defining a RuntimeRep-polymorphic identity does not work: myId1 :: forall (r :: RuntimeRep) (t :: TYPE r). t -> t myId1 x = x The GHC Users Guide explains why[1]. It's impossible to generate code for myId1 because there is no way of determining the machine representation of the argument x. But worse, it's not even possible to define a *Levity*-polymorphic identity: myId2 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)). t -> t myId2 x = x In this case the argument can only have kind TYPE LiftedRep or TYPE UnliftedRep. The machine representation is the same in each case. The problem this time is that the code generator doesn't know whether it should emit code to evaluate the argument (UnliftedRep case) or not (LiftedRep case). But this seems like a solvable problem. Surely a KnownLevity type class (possibly magical) could solve the problem. This seems like it should work myId3 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)). KnownLevity lev => t -> t myId3 x = x and in fact I wouldn't be surprised if this could be made to work: myId4 :: forall (r :: RuntimeRep) (t :: TYPE r). KnownRuntimeRep r => t -> t myId4 x = x So what is the situation here? 1. myId3 already works (then where is KnownLevity made available and why isn't it mentioned in the Users Guide?) 2. myId3 can never work (then why not?) 3. myId3 might be able to work but it's an open research problem (then who is working on it, if anyone?) 4. myId3 would work and it would be useful but no one's proposed or implemented it (then who would be the best person to collaborate with on that?) 5. myId3 would work but it would not actually be useful (then what have I misunderstood?) I suspect the answer is 1 (or maybe 4) based on the following passage in the Levity Polymorphism[2] paper by RE & SPJ[2]: > users can use a runtime type check (though GHC’s Typeable feature) > to determine the memory representation of an as-yet- unbound > argument to a function (and the same questions for myId4). Thanks, Tom [1] https://downloads.haskell.org/~ghc/9.4.4/docs/users_guide/exts/representati… [2] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/levity-…

5 8

[ANN] Copilot 3.13
by Ivan Perez 10 Jan '23

10 Jan '23

Dear all, I'm very excited to announce Copilot 3.13. Copilot is a stream-based DSL for writing and monitoring embedded C programs, with an emphasis on correctness and hard realtime requirements. Copilot is typically used as a high-level runtime verification framework, and supports temporal logic (LTL, PTLTL and MTL), clocks and voting algorithms. Among others, Copilot has been used at the Safety Critical Avionics Systems Branch of NASA Langley Research Center for monitoring test flights of drones. It also serves as a runtime monitoring backend for the requirements elicitation tool FRET (https://github.com/NASA-SW-VnV/fret/) via Ogma ( https://github.com/nasa/ogma) This release fixes 4 bugs in copilot-core and copilot-c99. We have also removed 2 deprecated modules and one dependency. The new release has been published on hackage, as well as github. Current emphasis is on increasing test coverage, removing unnecessary dependencies, hiding internal definitions, and formatting the code to meet our new coding standards. Users are encouraged to participate by opening issues and asking questions via our github repo ( https://github.com/copilot-language/copilot) I'd also like to take this opportunity to announce that Copilot is now being made available on Ubuntu Lunar 23.04 and Debian Bookworm. We would like to thank the Debian Haskell Group and, most especially, Scott Talbert, for continued effort making Copilot available on Debian-based distros. This will be extremely useful to a great portion of our users, who need to use Copilot as a runtime verification system targeting C, but do not need to become proficient in Haskell. We hope to continue this effort by making Copilot easily available on other distributions and OSs. Happy Haskelling, The Copilot team

1 0