4 ms·
[warning: ignorant musing of someone who doesn't know Scala below] This makes me wonder if 'values' can be though of as just subtypes of their types. '5' exten
by ajkjk 11y ago
[warning: ignorant musing of someone who doesn't know Scala below]
This makes me wonder if 'values' can be though of as just subtypes of their types. '5' extends 'Number', say. Is this how it's interpreted in the fully-functional paradigm?
If you have
def fn(x: Int) : Int
then 'Int' is the type of all Ints, and you have to provide a specific int - which is a subtype of Int, but you could imagine there being a subtype between 'Int' and '5', like:
5 <: intermediateType <: Int
So in order to 'invoke' a function you have to provide a subtype that reduces it to one value, at the level of 5, not just any subtype of int. Meaning that something about '5' makes it a special kind of subtype that can actually be used to execute the function. Maybe that's what we mean by 'value'. I don't know.
I do find the idea that fn(5) is a subtype of fn(x: Int) to be cute.
And that
def foo(x: Int): Int = fn(x)
has the 'subtype'
foo(5): fn(5)
seems suggestive.
- kryptiskt 11y agoYou may be interested in how Typed Racket does types. http://docs.racket-lang.org/ts-reference/type-ref.html http://docs.racket-lang.org/ts-reference/type-ref.html
- CHY872 11y agoFor a bit of theoretical background, try http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf (it's fairly easy reading). I'm not sure I quite understand what you're saying completely, but typically we distinguish types from values because we otherwise find it very difficult to write a performant typing algorithm. Personally, I try to avoid subtyping where possible; I usually end up getting weird contradictions.
- tel 11y agoThere's some significant sense to what you're talking about, so I'll share some pointers into deeper waters. The idea of a value being a type is the nature of "dependently typed" languages. However, they do it the other way around: types are merely values. This is very similar to what you're saying except DT languages would not have that 5 : 5 Instead, we introduce the idea of a singleton type. It works like this: for any type A and any value (x : A), we have a type (Sing A x) with exactly one value, (TheSing x : Sing A x). The other thing to keep in mind is that subtyping is kind of a rocky place to lay your type semantics. This is rough because most people are used to subtyping in their types. Instead, we note that whenever we have that (A :> B) then we have a function (A -> B) which is injective (really, an "epimorphism"). This broaden's our view to consider any injective function between types instead of merely some subtyping relation. Immediately it ought to be clear that (a) this is intractable automatically and (b) it's far more rich. Then it turns out that subtyping itself is fairly intractable (which subtypes are the right ones? there are many types intermediate between (Sing Integer 5) and (Integer)). So throw away automatic subsumption and require explicit coercions. This is workable and indeed in use today.
- ajkjk 11y agoThis is really interesting, thanks.
- seanmcdirmid 11y agoIt seems that you can either fight subtyping (by avoiding it) or embrace it; e.g. with pure subtype system: http://people.tamu.edu/~hiraditya/index_files/ProgLang_Presentation.pdf http://people.tamu.edu/~hiraditya/index_files/ProgLang_Prese... You do exchange a typing judgment for a subtyping one. I feel like we haven't really looked at subtyping enough. It might not be so hard as it is different, that our existing type systems simply aren't suited to it but we could come up with subtype systems that are.