[Haskell-cafe] Current state of type-level natural number programming

[Li-yao Xia]

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.