3 ms·
> My question remains. What's to stop me from coding invalid logic in my types? How do I test the logic? You test the logic the same way people have tested ter
by whateveracct 5y ago
> My question remains. What's to stop me from coding invalid logic in my types? How do I test the logic?
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."
At the term-level, you typically use equality to implement assert.
~ gives you a type-level "assertEqual" with which to write the exact same sort of unit tests you can write at the term level.
--
For the examples, you need to import GHC.TypeLits. It has the type family "+"
- 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.
- dmitriid 5y agoOkay, I finally made it compile. Let's revisit: > whateveracct: A concrete example > whateveracct: type AddTest = 2 + 2 ~ 4 > dmitriid: If you write 2 + 2 ~ 5, all types will be correct (Int), but the function will be incorrect. > whateveracct: If you write 2 + 2 ~ 5, your build will fail because your assertion failed. Just pasted this into https://replit.com/languages/haskell https://replit.com/languages/haskell, and of course it passed {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} import GHC.TypeLits; type AddTest = (2 + 2) ~ 5 main = putStrLn "Hello, World!"
- tome 5y agoYou haven't tested the type you wrote. `type AddTest = (2 + 2) ~ 5` compiles without error the same way `addTest = (2 + 2) == 5` would run without error. To test it, try, for example {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-} {-# LANGUAGE RankNTypes #-} import GHC.TypeLits test :: ((2 + 2) ~ 5 => a) -> a test x = x main = putStrLn "Hello, World!" That will fail to compile. If you change the 5 to 4 then it will compile.
- dmitriid 5y agoThank you! This leaves only the question of cost vs benefits of these approaches :)
- whateveracct 5y agomaybe a type Test (c :: Constraint) = c => () is in order here ;) testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = ()
- tome 5y agoThat compiles though. You need to CPS the constraint as in my example above. This does the job: type Test (c :: Constraint) = forall a. (c => a) -> a testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = id