So, your programming with types. Do you also write tests with types? ;)
In before "types check stuff". If you code some convoluted logic with types (and even non-convoluted logic, too), you still need to test that you've coded that logic correctly.
In before "types check stuff". If you code some convoluted logic with types (and even non-convoluted logic, too), you still need to test that you've coded that logic correctly.
In a real dependently-typed language the friction would be lower, because it's easier to put "normal code" at the type level.
Perhaps I could have skipped some type-level tests by introducing more kind-safety...
https://hackage.haskell.org/package/should-not-typecheck
https://www.scalatest.org/scaladoc/3.2.0/org/scalatest/match...
For example, a real-world situation from Turkey (looking at my check from Marks and Specner): goods from category 1 (clothes) have VAT of 8%, from category 2 have VAT of 18 % (plastic bag), and that if a person buys 2 items they get a 15% discount, and if they buy 3 items they get a 25% discount, and there are additional discounts on various goods.
This will type check even if you code it as "if there is 1 item, do a 40% discount, and assign VAT of 2%".
type Test1 = TypeExpressionImTesting ~ ExpectedType
A concrete example
type AddTest = 2 + 2 ~ 4
If you write 2 + 2 ~ 5, all types will be correct (Int), but the function will be incorrect.
So the question is: now you've coded significantly more difficult logic than adding two Ints together with types. How will you test that logic?
You can test more complicated logic the same way, using ~ as a type-level "shouldBe" that allows you to write type-level unit tests for said complicated logic.
So ~ tests not only the expected type, but the expected return value, too?
"A type context can include equality constraints of the form t1 ~ t2, which denote that the types t1 and t2 need to be the same." [1]
So. My question remains. What's to stop me from coding invalid logic in my types? How do I test the logic?
BTW, can't verify that "you can also easily check type-level computation as well." The example fails here https://replit.com/languages/haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
type AddTest = 2 + 2 ~ 4
main.hs:4:18: error: Not in scope: type constructor or class `+'
|
4 | type AddTest = 2 + 2 ~ 4
| ^
exit status 1
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 "+"
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
> 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, and of course it passed
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-}
import GHC.TypeLits;
type AddTest = (2 + 2) ~ 5
main = putStrLn "Hello, World!"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!"
This leaves only the question of cost vs benefits of these approaches :)
type Test (c :: Constraint) = c => ()
testTheObvious :: Test ((2 + 2) ~ 5)
testTheObvious = () type Test (c :: Constraint) = forall a. (c => a) -> a
testTheObvious :: Test ((2 + 2) ~ 5)
testTheObvious = id