About types - General

I've tried to understand types better but I find trouble. Quite complex things are understood but I wonder on basic level I don't understand types.

Best explanation seem to be that each type forms a game that has finite run time.

Type may also form ideas of what is equal under that type.

That sounds pretty abstract. I haven't heard types described that way before. I usually think of them as sets. Like the type Int is the set of fixed-precision integers, Bool is the set of booleans.

Sets are sufficient way to explain types for programming, but I've found it hard to explain through sets how types work.

what do you mean by "how types work"?

Types with lambda calculus result in a language that always terminates.

Hmm, I don't think that's fundamental in any way - you can always introduce some opaque fix :: forall r. (r -> r) -> r, which is well typed (in System F, which supports polymorphism)

so is your intuition for "how types work" somehow bound to termination? and why are sets bad for that?

Sets do not make it clear why types provide quarantee of termination. But if you take (x -> y) as a game where player has to play 'y' while opponent must play 'x'. You then see that any such finite combination of such game terminates.

but, afaik, there are also infinite games, and they are not that uncommon (e.g. chess could be one such game)

infinite games are also of interest in model theory, again - only afaik

I could probably take "finite sets" with the same success (although I'm almost certain you can still define undecidable/non-terminating stuff with finite sets)

It would be interesting to allow nontermination with type. How would that happen?

Haskell?

I think it's harder not to allow termination with types, and still have a "strong enough" programming language

Jonathan Knowles has marked this topic as resolved.

Jonathan Knowles has marked this topic as unresolved.