[blacktriangle]

So you're saying without dependent types you can express in a type a function that will return double each element in the list thus removing the need to test the function?

If you can do that, that's awesome, but I'm not seeing how.

[tsss]

I meant that you can write a version of your function with the same definition that will not type check since `take 2` is illegal for lists of length less than 2.

As for a function that will "double" a list, i.e. turn [1,2] into [1,1,2,2]: That is definitely possible with dependent types as they can express arbitrary statements. I'm not sure if you can do it without dependent types, but I'm inclined to say yes: something like an HList should work. Universal quantification over the HList parameters will ensure that the only way to create new values of the parameter types is to copy the old ones, as long as you disallow any form of `forall a. () -> a` in the type system.

Something like this, which is just the `double` function lifted into the universe of types, _might_ work, though its utility is questionable:

    type family DoubleList xs :: 'HList -> 'HList where
        DoubleCons ('HCons x ': xs) =  'HCons x ': 'HCons x ': Double xs
        DoubleNil 'HNil = 'HNil

[blacktriangle]

So totally different function, I meant by double to turn [1,2] into [2,4], however that's a really neat example. I hadn't seen the family extension in Haskell before. You're right there is a ton more to type systems than I was aware of. I was following some links in this thread and found this as well: https://www.parsonsmatt.org/2017/10/11/type_safety_back_and_....

I was less than impressed with type systems because like the blog post says, they tend to just kick the can down the road. The blog post uses a technique like you did in your example where rather than emitting more complicated type, they use the type system to protect the inputs of the function thus moving handling with the problem to the edges of the system which seems like a huge win. Between your example and that post I'm starting to see what people mean when they talk about programming in types, as its almost like the type system become a DSL with its own built-in test suite with which to program rather than a full programming language.

Either way very thought provoking, thank you for your responses.

[tsss]

> I meant by double to turn [1,2] into [2,4]

Hmm, I think you can do that too, but you'd have to assign each int value its own singleton type, which would be ridiculous and not gain you anything since you're just moving the logic up one level in the hierarchy of universes.

> what people mean when they talk about programming in types

If the type system is powerful enough then you can express any function at the type level. Some languages with universal polymorphism make no difference between types and terms. Any function can also be used at the type-level, kind-level and so on. Though usually just defining a simple wrapper type with smart constructor will get you 80% of the way in a business application with 2% of the effort of real type-level programming.