[Haskell-cafe] Is it possible to type a function to accept only literal values?

[Henning Thielemann]

On Tue, 27 Feb 2024, Daneel Yaitskov wrote:

> Recently I was experimenting with a GCC intrinsic functions for x86
> SMID instructions to write a fast CSV parser and noticed that some
> arguments are required to be literal values (known at compile time),
> which makes live hard, e.g. bit shift operation expects number of bits
> to shift in such a way.
> Nonetheless the intel manual defines function prototypes as normal:
>
>   __m128i _mm_bsrli_si128 (__m128i a, int imm8)
>
> Using a variable as second argument in _mm_bsrli_si128 produces
> unclear, but  compilation error with exact line number.
> Definitely some magic happens here, because it is not possible to
> express this constraint type system of C language.
>
> Haskell is known as one of the best languages in type acrobatics, but
> could it beat C here?

I'd use a type parameter instead of a value parameter. E.g.

bsrli :: M128I -> Proxy i -> M128I

using your favourite type-level natural number representation 'i'.

But actually, I would prevent doing vectorisation by hand and instead try 
to assist GCC to do the vectorization itself. This would work on all GCC 
supported target processors, not just one.