Is it possible to type a function to accept only literal values?
Hi List, 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? -- Best regards, Daniil Iaitskov
On Tue, Feb 27, 2024 at 12:32:48PM -0500, Daneel Yaitskov wrote:
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. [...] Haskell is known as one of the best languages in type acrobatics, but could it beat C here?
Sure, you can use Template Haskell for this. Use of `wellFormedBsrli` ensures that its second argument is always evaluated at compile time. See the output from GHC below for confirmation of this. Tom {-# LANGUAGE TemplateHaskell #-} module A where import Language.Haskell.TH import Language.Haskell.TH.Syntax bsrli :: Int -> Int -> Int bsrli = error "Implement bsrli here, using FFI, I guess" wellFormedBsrli :: Quote m => Int -> Code m (Int -> Int) wellFormedBsrli y = [|| \x -> bsrli x $$(liftTyped y) ||] {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -ddump-splices #-} module B where import A example :: Int example = $$(wellFormedBsrli (3 + 2)) 0x1 ghc B.hs -ddump-splices [1 of 2] Compiling A ( A.hs, A.o, A.dyn_o ) [Source file changed] [2 of 2] Compiling B ( B.hs, B.o, B.dyn_o ) [A[TH] changed] B.hs:9:5-29: Splicing expression wellFormedBsrli (3 + 2) ======> \ x_a2zf -> (bsrli x_a2zf) 5
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.
participants (3)
-
Daneel Yaitskov -
Henning Thielemann -
Tom Ellis