Quais são alguns casos de uso convincentes para tipos de métodos dependentes?

127

Os tipos de métodos dependentes, que antes eram um recurso experimental, agora foram ativados por padrão no porta-malas e, aparentemente, isso parece ter gerado algum entusiasmo na comunidade Scala.

À primeira vista, não é imediatamente óbvio para que isso poderia ser útil. Heiko Seeberger postou um exemplo simples de tipos de métodos dependentes aqui , que, como pode ser visto no comentário, podem ser facilmente reproduzidos com parâmetros de tipo em métodos. Portanto, esse não foi um exemplo muito convincente. (Talvez esteja faltando algo óbvio. Por favor, me corrija.)

Quais são alguns exemplos práticos e úteis de casos de uso para tipos de métodos dependentes, onde eles são claramente vantajosos sobre as alternativas?

Que coisas interessantes podemos fazer com eles que antes não eram possíveis / fáceis?

O que eles nos compram sobre os recursos existentes do sistema de tipos?

Além disso, os tipos de métodos dependentes são análogos ou inspiram-se em quaisquer recursos encontrados nos sistemas de tipos de outras linguagens de tipos avançadas, como Haskell, OCaml?

desaparecido
fonte
Você pode estar interessado em ler haskell.org/haskellwiki/Dependent_type
Dan Burton
Obrigado pelo link, Dan! Estou ciente dos tipos dependentes em geral, mas o conceito de tipos de métodos dependentes é relativamente novo para mim.
missingfaktor
Parece-me que "tipos de métodos dependentes" são simplesmente tipos que dependem de um ou mais tipos de entrada de um método (incluindo o tipo de objeto no qual o método é chamado); nada louco lá além da idéia geral de tipos dependentes. Talvez esteja faltando alguma coisa?
Dan Burton
Não, você não fez, mas aparentemente eu fiz. :-) Eu não vi o link entre os dois antes. Agora é claro como cristal.
Home

Respostas:

112

Mais ou menos, qualquer uso de tipos de membros (ou seja, aninhados) pode gerar uma necessidade de tipos de métodos dependentes. Em particular, sustento que, sem tipos de métodos dependentes, o padrão clássico de bolos está mais próximo de ser um anti-padrão.

Então qual é o problema? Os tipos aninhados no Scala dependem de sua instância anexa. Consequentemente, na ausência de tipos de métodos dependentes, as tentativas de usá-los fora dessa instância podem ser frustrantemente difíceis. Isso pode transformar projetos que inicialmente parecem elegantes e atraentes em monstruosidades que são terrivelmente rígidas e difíceis de refatorar.

Ilustrarei isso com um exercício que faço durante meu curso de treinamento Advanced Scala ,

trait ResourceManager {
  type Resource <: BasicResource
  trait BasicResource {
    def hash : String
    def duplicates(r : Resource) : Boolean
  }
  def create : Resource

  // Test methods: exercise is to move them outside ResourceManager
  def testHash(r : Resource) = assert(r.hash == "9e47088d")  
  def testDuplicates(r : Resource) = assert(r.duplicates(r))
}

trait FileManager extends ResourceManager {
  type Resource <: File
  trait File extends BasicResource {
    def local : Boolean
  }
  override def create : Resource
}

class NetworkFileManager extends FileManager {
  type Resource = RemoteFile
  class RemoteFile extends File {
    def local = false
    def hash = "9e47088d"
    def duplicates(r : Resource) = (local == r.local) && (hash == r.hash)
  }
  override def create : Resource = new RemoteFile
}

É um exemplo do padrão clássico de bolos: temos uma família de abstrações que são gradualmente refinadas através de uma hierarquia ( ResourceManager/ Resourcesão refinadas por FileManager/ Fileque, por sua vez, são refinadas por NetworkFileManager/ RemoteFile). É um exemplo de brinquedo, mas o padrão é real: é usado em todo o compilador Scala e foi amplamente utilizado no plug-in Scala Eclipse.

Aqui está um exemplo da abstração em uso,

val nfm = new NetworkFileManager
val rf : nfm.Resource = nfm.create
nfm.testHash(rf)
nfm.testDuplicates(rf)

Note-se que os meios de dependência caminho que o compilador irá garantir que o testHashe testDuplicatesmétodos on NetworkFileManagersó pode ser chamado com argumentos que correspondem a ele, ou seja. é próprio RemoteFilese nada mais.

É inegavelmente uma propriedade desejável, mas suponha que desejássemos mover esse código de teste para um arquivo de origem diferente? Com tipos de métodos dependentes, é fácil redefinir esses métodos fora da ResourceManagerhierarquia,

def testHash4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.hash == "9e47088d")

def testDuplicates4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.duplicates(r))

Observe os usos dos tipos de métodos dependentes aqui: o tipo do segundo argumento ( rm.Resource) depende do valor do primeiro argumento ( rm).

É possível fazer isso sem tipos de métodos dependentes, mas é extremamente incômodo e o mecanismo é pouco intuitivo: eu ensino este curso há quase dois anos e, nesse período, ninguém encontrou uma solução que funcionasse sem ser solicitada.

Experimente você mesmo ...

// Reimplement the testHash and testDuplicates methods outside
// the ResourceManager hierarchy without using dependent method types
def testHash        // TODO ... 
def testDuplicates  // TODO ...

testHash(rf)
testDuplicates(rf)

Depois de um breve período de dificuldade, você provavelmente descobrirá por que eu (ou talvez tenha sido David MacIver, não podemos lembrar qual de nós cunhou o termo) a chamo de Padaria da Perdição.

Edit: consenso é que Bakery of Doom foi cunhagem de David MacIver ...

Para o bônus: a forma de tipos dependentes de Scala em geral (e tipos de métodos dependentes como parte dela) foi inspirada pela linguagem de programação Beta ... elas surgem naturalmente da semântica consistente de nidificação de Beta. Eu não conheço nenhuma outra linguagem de programação, mesmo que levemente convencional, que tenha tipos dependentes neste formulário. Idiomas como Coq, Cayenne, Epigram e Agda têm uma forma diferente de digitação dependente, que de certa forma é mais geral, mas que difere significativamente por fazer parte de sistemas de tipos que, diferentemente do Scala, não possuem subtipo.

Miles Sabin
fonte
2
Foi David MacIver quem cunhou o termo, mas, de qualquer forma, é bastante descritivo. Essa é uma explicação fantástica do motivo pelo qual os tipos de métodos dependentes são tão interessantes. Bom trabalho!
Daniel Spiewak
Ele surgiu inicialmente em uma conversa entre nós dois no #scala há algum tempo ... como eu disse, não me lembro qual de nós foi quem disse primeiro.
Miles Sabin
Parece que minha memória estava pregando peças em mim ... o consenso é que era a moeda de David MacIver.
Miles Sabin
Sim, eu não estava lá (no #scala) na época, mas Jorge estava e foi aí que eu estava obtendo minhas informações.
Daniel Spiewak
Utilizando o refinamento de membro do tipo abstrato, pude implementar a função testHash4 de maneira bastante simples. def testHash4[R <: ResourceManager#BasicResource](rm: ResourceManager { type Resource = R }, r: R) = assert(r.hash == "9e47088d")Suponho que isso possa ser considerado outra forma de tipos dependentes, no entanto.
Marco van Hilst
53
trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}

Em outro lugar, podemos garantir estaticamente que não estamos misturando nós de dois gráficos diferentes, por exemplo:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 

Obviamente, isso já funcionou se definido por dentro Graph, mas dizemos que não podemos modificar Graphe estamos escrevendo uma extensão "pimp my library" para ela.

Sobre a segunda pergunta: os tipos ativados por esse recurso são muito mais fracos que os tipos dependentes completos (consulte Programação dependente de tipos no Agda para obter uma amostra disso.) Acho que nunca vi uma analogia antes.

Alexey Romanov
fonte
6

Esse novo recurso é necessário quando membros do tipo abstrato concreto são usados ​​em vez de parâmetros de tipo . Quando parâmetros de tipo são usados, a dependência do tipo de polimorfismo da família pode ser expressa nas versões mais recentes e mais antigas do Scala, como no exemplo simplificado a seguir.

trait C[A]
def f[M](a: C[M], b: M) = b
class C1 extends C[Int]
class C2 extends C[String]

f(new C1, 0)
res0: Int = 0
f(new C2, "")
res1: java.lang.String = 
f(new C1, "")
error: type mismatch;
 found   : C1
 required: C[Any]
       f(new C1, "")
         ^
Shelby Moore III
fonte
Isso não tem relação. Com membros do tipo, você pode usar refinamentos para o mesmo resultado: trait C {type A}; def f[M](a: C { type A = M}, b: M) = 0;class CI extends C{type A=Int};class CS extends C{type A=String}etc.
nafg
De qualquer forma, isso não tem nada a ver com tipos de métodos dependentes. Tomemos, por exemplo, o exemplo de Alexey ( stackoverflow.com/a/7860821/333643 ). Usar sua abordagem (incluindo a versão de refinamento que comentei) não atinge a meta. Isso garantirá que n1.Node =: = n2.Node, mas não garantirá que ambos estejam no mesmo gráfico. O IIUC DMT garante isso.
nafg
@nafg Obrigado por apontar isso. Adicionei a palavra concreto para deixar claro que não estava me referindo ao caso de refinamento para os membros do tipo. Até onde posso ver, esse ainda é um caso de uso válido para tipos de métodos dependentes, apesar do seu argumento (que eu sabia) de que eles podem ter mais poder em outros casos de uso. Ou eu perdi a essência fundamental do seu segundo comentário?
Shelby Moore III #
3

Estou desenvolvendo um modelo para a interoperabilidade de uma forma de programação declarativa com o estado ambiental. Os detalhes não são relevantes aqui (por exemplo, detalhes sobre retornos de chamada e semelhança conceitual com o modelo do ator combinado com um serializador).

O problema relevante é que os valores de estado são armazenados em um mapa de hash e referenciados por um valor de chave de hash. As funções inserem argumentos imutáveis ​​que são valores do ambiente, podem chamar outras funções e gravar estado no ambiente. Mas as funções são não permissão para ler valores do ambiente (portanto, o código interno da função não depende da ordem das mudanças de estado e, portanto, permanece declarativo nesse sentido). Como digitar isso no Scala?

A classe de ambiente deve ter um método sobrecarregado que insira uma função para chamar e insira as chaves hash dos argumentos da função. Portanto, esse método pode chamar a função com os valores necessários no mapa de hash, sem fornecer acesso público de leitura aos valores (portanto, conforme necessário, negar às funções a capacidade de ler valores do ambiente).

Mas, se estas chaves de hash são cadeias ou valores hash inteiros, a tipagem estática do hash mapa elemento tipo engloba a qualquer ou AnyRef (código mapa hash não mostrado abaixo), e, assim, um desfasamento de tempo de execução poderia ocorrer, ou seja, seria possível para colocar qualquer tipo de valor em um mapa de hash para uma determinada chave de hash.

trait Env {
...
  def callit[A](func: Env => Any => A, arg1key: String): A
  def callit[A](func: Env => Any => Any => A, arg1key: String, arg2key: String): A
}

Embora eu não tenha testado o seguinte, em teoria eu posso obter as chaves de hash dos nomes das classes em tempo de execução classOf, portanto, uma chave de hash é um nome de classe em vez de uma string (usando os backticks de Scala para incorporar uma string em um nome de classe).

trait DependentHashKey {
  type ValueType
}
trait `the hash key string` extends DependentHashKey {
  type ValueType <: SomeType
}

Assim, a segurança do tipo estático é alcançada.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A
Shelby Moore III
fonte
Quando precisamos passar as chaves de argumento em um único valor, não testei, mas suponha que possamos usar uma Tupla, por exemplo, para a sobrecarga de 2 argumentos def callit[A](argkeys: Tuple[DependentHashKey,DependentHashKey])(func: Env => argkeys._0.ValueType => argkeys._1.ValueType => A): A. Não usaríamos uma coleção de chaves de argumento, porque os tipos de elemento seriam incluídos (desconhecidos no momento da compilação) no tipo de coleção.
Shelby Moore III
"a digitação estática do tipo de elemento do mapa de hash é incluída em Any ou AnyRef" - eu não sigo. Quando você diz o tipo de elemento, quer dizer o tipo de chave ou o tipo de valor (ou seja, o primeiro ou o segundo tipo de argumento para o HashMap)? E por que isso seria absorvido?
Robin Green
@RobinGreen O tipo dos valores na tabela de hash. Caso, incluído porque você não pode colocar mais de um tipo em uma coleção no Scala, a menos que você inclua o supertipo comum, porque o Scala não tem um tipo de união (disjunção). Veja minhas perguntas e respostas sobre subsunção em Scala.
Shelby Moore III