<p>In my interpretation of how Scala types can be translated to type theory,
a trait is a type and an instance of the trait is a subtype. Therefore, in the example above, <code>Entry</code> would be:
<span class="math-container">$$\mathit{Entry} = \Sigma\mathit{Key} : *. \mathit{Key}$$</span>
Notice that this is a dependent sum type (or existential, if you prefer); the first element (<code>Key</code>) is a type  and the second (<code>key</code>) is a value of this type.</p>
<p>Then, the <code>extractKey</code> method would be translated to:
<span class="math-container">$$
\mathrm{extractKey} :: \Pi e : \mathit{Entry}. \mathrm{fst}(e) \\
\mathrm{extractKey} = \lambda e : \mathit{Entry}. \mathrm{snd}(e)
$$</span>
As I see it, this is indeed a dependent function.</p>
<p>This translation relies on subtyping for passing instances of the trait <span class="math-container">$\mathit{Entry}$</span> to this function. For example, if <span class="math-container">$E \sqsubseteq \mathit{Entry}$</span> is a class &quot;extending&quot; the trait (I hope I'm correctly using Scala terminology here), then a value <span class="math-container">$e :: E$</span> would also have the type <span class="math-container">$e :: \mathit{Entry}$</span> and could be passed to <span class="math-container">$\mathrm{extractKey}$</span>.</p>
<p>If you want to make this subtype polymorphism more explicit, as I believe was your intention in the question, then it would be:
<span class="math-container">$$
\mathrm{extractKey} :: \forall E \sqsubseteq \mathit{Entry}. \Pi e : E. \mathrm{fst}(e) \\
\mathrm{extractKey} = \Lambda E \sqsubseteq \mathit{Entry}. \lambda e : E. \mathrm{snd}(e)
$$</span>
and again you'd have a dependent function.</p>

CC BY-SA 4.0
2024-01-03T23:28:14.677Z
2024-01-03T23:28:14.677Z
nickie
<p>I am learning Scala 3 and so far I am really enjoying it. I was going through its <a href="https://docs.scala-lang.org/scala3/reference/index.html" rel="nofollow noreferrer">reference documentation</a> and I noticed that it claims to have <a href="https://docs.scala-lang.org/scala3/reference/new-types/dependent-function-types.html" rel="nofollow noreferrer">dependent function types</a>. This feels misleading to me because the terminology &quot;dependent function type&quot; is more commonly associated with Π-types (<a href="https://ncatlab.org/nlab/show/calculus+of+constructions" rel="nofollow noreferrer">Calculus of Constructions</a>, <a href="https://ncatlab.org/nlab/show/pure+type+system" rel="nofollow noreferrer">Pure Type Systems</a>) whereas Scala's dependent function types seem to be just plain old return-type polymorphism.</p>
<p>The reference documentation presents the following example:</p>
<pre><code>trait Entry { type Key; val key: Key }

def extractKey(e: Entry): e.Key = e.key          // a dependent method

val extractor: (e: Entry) =&gt; e.Key = extractKey  // a dependent function value
//             ^^^^^^^^^^^^^^^^^^^
//             a dependent function type
</code></pre>
<p>In this example, the type of <code>def extractKey</code> could be rewritten as <code>def extractKey[E: Entry](e: E): E.Key = e.key</code>: the dependency on <code>e</code> is artificial since the value itself is not mentioned in the return type of <code>extractKey</code> in any way other than as a path to the concrete type that was abstracted away by the trait.</p>
<p>Am I off base here or does this &quot;Scala 3 has dependent function types&quot; claim sound fishy?</p>

CC BY-SA 4.0
2024-01-02T23:35:49.970Z
"Could be rewritten as" is true for a lot of things. What does of a list of `Entry`s look like if you re-write it?
cody
CC BY-SA 4.0
2024-01-03T14:03:09.277Z
@cody If Scala's "dependent function types" were really dependent then appending [this class](https://scastie.scala-lang.org/VbMgJvzFTKiuyhUvPboHvQ) to the previous example should have been able to compile, no? This fails even before type checking, it fails at parsing.
Valmir Junior
CC BY-SA 4.0
2024-01-03T22:19:47.760Z
Scala 3 doesn't have full dependent types, but only *path dependent types*, which is a weaker form of dependency. They allow values (e.g. objects) to carry types along with them, and these types can be used in type-checking.
Martin Berger
<calculus-of-constructions>
Isn't it misleading for Scala 3 to claim it has dependent function types?
Valmir Junior
# Isn't it misleading for Scala 3 to claim it has dependent function types?

(Asked by: username_0 on 2024-01-02)

I am learning Scala 3 and so far I am really enjoying it. I was going through its reference documentation and I noticed that it claims to have dependent function types. This feels misleading to me because the terminology "dependent function type" is more commonly associated with Π-types (Calculus of Constructions, Pure Type Systems) whereas Scala's dependent function types seem to be just plain old return-type polymorphism.
The reference documentation presents the following example:
trait Entry { type Key; val key: Key }

def extractKey(e: Entry): e.Key = e.key          // a dependent method

val extractor: (e: Entry) => e.Key = extractKey  // a dependent function value
//             ^^^^^^^^^^^^^^^^^^^
//             a dependent function type

In this example, the type of def extractKey could be rewritten as def extractKey[E: Entry](e: E): E.Key = e.key: the dependency on e is artificial since the value itself is not mentioned in the return type of extractKey in any way other than as a path to the concrete type that was abstracted away by the trait.
Am I off base here or does this "Scala 3 has dependent function types" claim sound fishy?

**Tags:** calculus-of-constructions
> **Comments:**
> **username_1**: "Could be rewritten as" is true for a lot of things. What does of a list of `Entry`s look like if you re-write it?  
> **username_0**: @cody If Scala's "dependent function types" were really dependent then appending [this class](https://scastie.scala-lang.org/VbMgJvzFTKiuyhUvPboHvQ) to the previous example should have been able to compile, no? This fails even before type checking, it fails at parsing.  
> **username_2**: Scala 3 doesn't have full dependent types, but only *path dependent types*, which is a weaker form of dependency. They allow values (e.g. objects) to carry types along with them, and these types can be used in type-checking.  

---

## 1 answers

### Answer by username_3 on 2024-01-03. Score: 2 | Accepted answer

In my interpretation of how Scala types can be translated to type theory,
a trait is a type and an instance of the trait is a subtype. Therefore, in the example above, `Entry` would be:
$$\mathit{Entry} = \Sigma\mathit{Key} : \*. \mathit{Key}$$
Notice that this is a dependent sum type (or existential, if you prefer); the first element (`Key`) is a type and the second (`key`) is a value of this type.

Then, the `extractKey` method would be translated to:
$$
\mathrm{extractKey} :: \Pi e : \mathit{Entry}. \mathrm{fst}(e) \\
\mathrm{extractKey} = \lambda e : \mathit{Entry}. \mathrm{snd}(e)
$$
As I see it, this is indeed a dependent function.

This translation relies on subtyping for passing instances of the trait $\mathit{Entry}$ to this function. For example, if $E \sqsubseteq \mathit{Entry}$ is a class "extending" the trait (I hope I'm correctly using Scala terminology here), then a value $e :: E$ would also have the type $e :: \mathit{Entry}$ and could be passed to $\mathrm{extractKey}$.

If you want to make this subtype polymorphism more explicit, as I believe was your intention in the question, then it would be:
$$
\mathrm{extractKey} :: \forall E \sqsubseteq \mathit{Entry}. \Pi e : E. \mathrm{fst}(e) \\
\mathrm{extractKey} = \Lambda E \sqsubseteq \mathit{Entry}. \lambda e : E. \mathrm{snd}(e)
$$
and again you'd have a dependent function.


---

