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.