4 ms·
> You test the logic the same way people have tested term-level logic for years. You say "this call to my function with these args results in this output." Wha
by dmitriid 5y ago
> You test the logic the same way people have tested term-level logic for years. You say "this call to my function with these args results in this output."
What is the value of adding this to types then? Besides increasing compilation time?
> For the examples, you need
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits;
type AddTest = 2 + 2 ~ 4
main.hs:5:20: error:
* Expected kind `Nat', but `2 ~ 4' has kind `Constraint'
* In the second argument of `(+)', namely `2 ~ 4'
In the type `2 + 2 ~ 4'
In the type declaration for `AddTest'
|
5 | type AddTest = 2 + 2 ~ 4
| ^^^^^
exit status 1
So far "easily check type-level computation as well" fails to be easy.