Current state of type-level natural number programming

newer
Re: [Haskell-cafe] Current state...

Henning Thielemann

11 Jan 2023 11 Jan '23

9:55 a.m.

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?

Show replies by date

Li-yao Xia

11 Jan 11 Jan

2:07 p.m.

New subject: Current state of type-level natural number programming

Hi Henning, Liquid Haskell may be what you're looking for. On 2023-01-11 2:55 PM, Henning Thielemann wrote:

...

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? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Dan Dart

12 Jan 12 Jan

12:24 p.m.

Hey! I had a go at this too the other week and came across the same >= == problem you're having. I'm not sure if it's doable this way without dependent types, but maybe typed unary would work. I found a good video series to study by Richard A. Eisenberg. He mentions typed unary numbers and goes over existentials such that he doesn't have the same problem. https://www.youtube.com/watch?v=PHS3Q-tRjFQ https://www.youtube.com/watch?v=WHeBxSBY0fc https://www.youtube.com/watch?v=dK5be4cdQdE https://www.youtube.com/watch?v=8AKtqFY1ueM https://www.youtube.com/watch?v=jPZciAJ0oaw https://www.youtube.com/watch?v=S5Oz_w9HDs0 Hope that helps Dan Dart

Henning Thielemann

12:49 p.m.

New subject: Current state of type-level natural number programming

On Thu, 12 Jan 2023, Dan Dart wrote:

...

I had a go at this too the other week and came across the same >= == problem you're having.

I'm not sure if it's doable this way without dependent types, but maybe typed unary would work. I found a good video series to study by Richard A. Eisenberg. He mentions typed unary numbers and goes over existentials such that he doesn't have the same problem.

So far I am using type-level decimal numbers of the 'tfp' package. My numbers can become a bit bigger, like 256 or 512, so Unary might be too slow.

石井大海

1:05 p.m.

New subject: Current state of type-level natural number programming

Hi,

...

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" "Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"

So, what is the current state of the art? What libraries, what GHC extensions? Any tutorials?

Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code: https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger Formally, this augments GHC's type checker with Presburger Arithmetic Solver. https://en.wikipedia.org/wiki/Presburger_arithmetic In other words, the plugin can solve propositions in natural number arithmetic which incorporates only addition, subtraction, inequalities and constant-factor multiplication. This fragment of Peano arithmetic is known to be decidable (note that it cannot solve the proposition incorporating arbitrary (indefinite) multiplications to avoid incompleteness hell). Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences. Thanks, -- Hiromi ISHII konn.jinro@gmail.com

...

2023/01/11 23:55、Henning Thielemann のメール:

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? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Henning Thielemann

1:10 p.m.

New subject: Current state of type-level natural number programming

On Fri, 13 Jan 2023, 石井大海 wrote:

...

Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:

https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger

Formally, this augments GHC's type checker with Presburger Arithmetic Solver.

This sounds promising! I know that Iavor Diatchki implemented a Presburger Arithmetic Solver for GHC type checking many years ago, but when I asked last time, he recommended ghc-typelits-natnormalise.

...

Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences.

It is good to know that I can combine different type checker plugins.

rowan goemans

13 Jan 13 Jan

3:32 a.m.

New subject: Current state of type-level natural number programming

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))) foo :: (n ~ 0) => Int foo = 10 bar :: forall (n :: Nat). (n <= 0) => Int bar = case nLEZeroIsZeroRule @n of { Sub Dict -> foo @n } If you can hide your contraints behind this for users of your library it might not such a bad option. I don't need very many of these since natnormalise does by far the most work for me. This just fills the gaps. Rowan Goemans On 1/12/23 19:10, Henning Thielemann wrote:

...

On Fri, 13 Jan 2023, 石井大海 wrote:

...
Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:

https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger

Formally, this augments GHC's type checker with Presburger Arithmetic Solver.

This sounds promising!

I know that Iavor Diatchki implemented a Presburger Arithmetic Solver for GHC type checking many years ago, but when I asked last time, he recommended ghc-typelits-natnormalise.

...
Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences.

It is good to know that I can combine different type checker plugins.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

859

Age (days ago)

861

Last active (days ago)

List overview

Download

6 comments

5 participants

participants (5)

Dan Dart
Henning Thielemann
Li-yao Xia
rowan goemans
石井大海