Alguma razão pela qual o scala não suporta explicitamente tipos dependentes?

Existem tipos dependentes de caminho e acho que é possível expressar quase todos os recursos de linguagens como Epigram ou Agda em Scala, mas estou me perguntando por que Scala não suporta isso de forma mais explícita como faz muito bem em outras áreas (digamos , DSLs)? Algo que estou perdendo como "não é necessário"?

Conveniência sintática à parte, a combinação de tipos singleton, tipos dependentes de caminho e valores implícitos significa que Scala tem um suporte surpreendentemente bom para tipagem dependente, como tentei demonstrar no sem forma .

O suporte intrínseco do Scala para tipos dependentes é por meio de tipos dependentes de caminho . Isso permite que um tipo dependa de um caminho de seletor através de um gráfico de objeto (ou seja, valor), assim,

scala> class Foo { class Bar }
defined class Foo

scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658

scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757

scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>

scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
              implicitly[foo1.Bar =:= foo2.Bar]

Em minha opinião, o que foi dito acima deve ser suficiente para responder à pergunta "Scala é uma linguagem de tipo dependente?" no positivo: é claro que aqui temos tipos que se distinguem pelos valores que são seus prefixos.

No entanto, muitas vezes é objetado que Scala não é uma linguagem de tipo "totalmente" dependente porque não tem soma dependente e tipos de produto como encontrados em Agda ou Coq ou Idris como intrínsecos. Acho que isso reflete uma fixação na forma sobre os fundamentos até certo ponto, no entanto, tentarei mostrar que o Scala está muito mais próximo dessas outras linguagens do que normalmente se reconhece.

Apesar da terminologia, os tipos de soma dependentes (também conhecidos como tipos Sigma) são simplesmente um par de valores em que o tipo do segundo valor depende do primeiro valor. Isso é diretamente representável no Scala,

scala> trait Sigma {
     |   val foo: Foo
     |   val bar: foo.Bar
     | }
defined trait Sigma

scala> val sigma = new Sigma {
     |   val foo = foo1
     |   val bar = new foo.Bar
     | }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8

e, de fato, essa é uma parte crucial da codificação de tipos de métodos dependentes que são necessários para escapar da 'Padaria da Destruição' em Scala antes de 2.10 (ou anterior por meio da opção de compilador Scala experimental -Ydependent-method types).

Os tipos de produtos dependentes (também conhecidos como tipos Pi) são essencialmente funções de valores para tipos. Eles são a chave para a representação de vetores de tamanho estático e os outros filhos do pôster para linguagens de programação com tipos dependentes. Podemos codificar tipos Pi no Scala usando uma combinação de tipos dependentes de caminho, tipos singleton e parâmetros implícitos. Primeiro, definimos um traço que vai representar uma função de um valor do tipo T para um tipo U,

scala> trait Pi[T] { type U }
defined trait Pi

Podemos então definir um método polimórfico que usa este tipo,

scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]

(observe o uso do tipo dependente do caminho pi.Uno tipo de resultado List[pi.U]). Dado um valor do tipo T, esta função retornará uma lista (n vazia) de valores do tipo correspondente a esse valor T específico.

Agora vamos definir alguns valores adequados e testemunhas implícitas para as relações funcionais que queremos manter,

scala> object Foo
defined module Foo

scala> object Bar
defined module Bar

scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11

scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae

E agora aqui está nossa função de uso do tipo Pi em ação,

scala> depList(Foo)
res2: List[fooInt.U] = List()

scala> depList(Bar)
res3: List[barString.U] = List()

scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>

scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
              implicitly[res2.type <:< List[String]]
                    ^

scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>

scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
              implicitly[res3.type <:< List[Int]]

(observe que aqui usamos o <:<operador de testemunha de subtipo de Scala em vez de =:=porque res2.typee res3.typesão tipos singleton e, portanto, mais precisos do que os tipos que verificamos no RHS).

Na prática, entretanto, em Scala não começaríamos codificando os tipos Sigma e Pi e continuando daí como faríamos em Agda ou Idris. Em vez disso, usaríamos tipos dependentes de caminho, tipos singleton e implícitos diretamente. Você pode encontrar vários exemplos de como isso funciona sem forma: tipos de tamanhos , registros extensíveis , HLists abrangentes , retire seu clichê , Zíperes genéricos etc. etc.

A única objeção remanescente que posso ver é que na codificação acima dos tipos Pi exigimos que os tipos singleton dos valores dependentes sejam expressos. Infelizmente, em Scala, isso só é possível para valores de tipos de referência e não para valores de tipos sem referência (esp. Por exemplo, Int). Isto é uma vergonha, mas não uma dificuldade intrínseca: verificador de tipos de Scala representa os tipos únicos de valores não-referência internamente, e tem havido um par de experimentos em fazê-los diretamente expresso. Na prática, podemos contornar o problema com uma codificação de nível de tipo razoavelmente padrão dos números naturais .

Em qualquer caso, não acho que esta pequena restrição de domínio possa ser usada como uma objeção ao status do Scala como uma linguagem de tipo dependente. Se for, então o mesmo poderia ser dito para Dependent ML (que só permite dependências em valores de números naturais), o que seria uma conclusão bizarra.

Eu diria que é porque (como sei por experiência, tendo usado tipos dependentes no assistente de prova Coq, que os suporta totalmente, mas ainda não de uma forma muito conveniente) tipos dependentes são um recurso de linguagem de programação muito avançado que é realmente difícil de acertar - e pode causar uma explosão exponencial na complexidade na prática. Eles ainda são um tópico de pesquisa em ciência da computação.

Eu acredito que os tipos dependentes de caminho do Scala só podem representar tipos Σ, mas não tipos Π. Este:

trait Pi[T] { type U }

não é exatamente um tipo Π. Por definição, tipo Π, ou produto dependente, é uma função cujo tipo de resultado depende do valor do argumento, representando o quantificador universal, ou seja, ∀x: A, B (x). No caso acima, entretanto, depende apenas do tipo T, mas não de algum valor desse tipo. O traço Pi em si é um tipo Σ, um quantificador existencial, ou seja, ∃x: A, B (x). A autorreferência do objeto, neste caso, está atuando como variável quantificada. Quando passado como parâmetro implícito, entretanto, ele se reduz a uma função de tipo comum, uma vez que é resolvido por tipo. A codificação para o produto dependente no Scala pode ser parecida com a seguinte:

trait Sigma[T] {
  val x: T
  type U //can depend on x
}

// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U 

A peça que falta aqui é a capacidade de restringir estaticamente o campo x ao valor esperado t, efetivamente formando uma equação que representa a propriedade de todos os valores que habitam o tipo T. Junto com nossos Σ-tipos, usados ​​para expressar a existência de objeto com determinada propriedade, o a lógica é formada, na qual nossa equação é um teorema a ser provado.

Por outro lado, no caso real, o teorema pode ser altamente não trivial, até o ponto em que não pode ser derivado automaticamente do código ou resolvido sem uma quantidade significativa de esforço. Pode-se até formular a hipótese de Riemann dessa forma, apenas para descobrir que a assinatura é impossível de implementar sem realmente prová-la, fazendo um loop para sempre ou lançando uma exceção.

A questão era sobre como usar o recurso de digitação dependente de forma mais direta e, na minha opinião, haveria uma vantagem em ter uma abordagem de tipagem dependente mais direta do que a que Scala oferece.
As respostas atuais tentam argumentar a questão em nível teórico de tipo. Eu quero dar um toque mais pragmático nisso. Isso pode explicar por que as pessoas estão divididas no nível de suporte dos tipos dependentes na linguagem Scala. Podemos ter em mente definições um tanto diferentes. (não quer dizer que um esteja certo e o outro errado).

Esta não é uma tentativa de responder à questão de quão fácil seria transformar Scala em algo como Idris (imagino que seja muito difícil) ou escrever uma biblioteca que ofereça suporte mais direto para recursos do tipo Idris (como singletonstenta estar em Haskell).

Em vez disso, quero enfatizar a diferença pragmática entre Scala e uma linguagem como Idris.
O que são bits de código para expressões de nível de valor e tipo? Idris usa o mesmo código, Scala usa um código muito diferente.

Scala (semelhante a Haskell) pode ser capaz de codificar muitos cálculos de nível de tipo. Isso é mostrado por bibliotecas como shapeless. Essas bibliotecas fazem isso usando alguns truques realmente impressionantes e inteligentes. No entanto, seu código de nível de tipo é (atualmente) bastante diferente das expressões de nível de valor (acho que essa lacuna é um pouco mais próxima em Haskell). Idris permite usar a expressão de nível de valor no nível de tipo COMO ESTÁ.

O benefício óbvio é a reutilização de código (você não precisa codificar expressões de nível de tipo separadamente do nível de valor se precisar delas em ambos os lugares). Deve ser muito mais fácil escrever código de nível de valor. Deve ser mais fácil não ter que lidar com hacks como singletons (sem mencionar o custo de desempenho). Você não precisa aprender duas coisas, você aprende uma coisa. Em um nível pragmático, acabamos precisando de menos conceitos. Digite sinônimos, digite famílias, funções, ... que tal apenas funções? Na minha opinião, esses benefícios de unificação são muito mais profundos e são mais do que conveniência sintática.

Considere o código verificado. Veja:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
O verificador de tipo verifica as provas das leis monádicas / functor / aplicativas e as provas são sobre reais implementações de monad / functor / aplicative e não algum equivalente de nível de tipo codificado que pode ser o mesmo ou não o mesmo. A grande questão é o que estamos provando?

O mesmo pode ser feito usando truques de codificação inteligentes (veja o seguinte para a versão Haskell, eu não vi um para Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https: // github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
exceto que os tipos são tão complicados que é difícil ver as leis, as expressões de nível de valor são convertidas (automaticamente, mas ainda assim) para coisas de nível de tipo e você precisa confiar nessa conversão também . Há espaço para erros em tudo isso, o que meio que desafia o propósito do compilador agir como um assistente de prova.

(EDITADO em 10/08/2018) Falando em assistência de prova, aqui está outra grande diferença entre Idris e Scala. Não há nada no Scala (ou Haskell) que possa impedir a redação de provas divergentes:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

enquanto o Idris tem uma totalpalavra - chave que impede a compilação de códigos como este.

Uma biblioteca Scala que tenta unificar valor e código de nível de tipo (como Haskell singletons) seria um teste interessante para o suporte de Scala de tipos dependentes. Essa biblioteca pode ser feita muito melhor no Scala por causa dos tipos dependentes de caminho?

Eu sou muito novo no Scala para responder a essa pergunta sozinho.