On Thu, Aug 19, 2021, at 06:14, Simon Peyton Jones wrote:
| We use types to communicate the externally-visible behavior of our | programs: the number of arguments to a function and their types, effects | incurred in the form of monads, etc. Why should liftedness and the | implications for evaluation strategies be different?
We use them to *communicate* behaviour, but not to *specify* behaviour. That is done by the definition of the function itself.
I disagree, types are a great specification language. The whole point of advanced type system features is to enhance the specification language so we can specify more interesting properties. Often, we do this so that the type checker can *verify* our code, but there are plenty of cases where we use types to *drive code generation*. Consider GHC.Generics. We can write a highly-polymorphic JSON serialization function gToJSON :: Generic a => a -> JSON which we can then instantiate at different types, e.g. data Foo fooToJSON :: Foo -> JSON fooToJSON = gToJSON data Bar barToJSON :: Bar -> JSON barToJSON = gToJSON fooToJSON and barToJSON have the exact same definition, but very different semantics. Their complete semantics depends on *both* their definition *and* their type signatures. I think the deeper point here is that Haskell's dynamic semantics depends on its static semantics. We can't evaluate a Haskell program without knowing the types involved.