Eu sei que Haskell já tem a capacidade de parametrizar um tipo sobre outro tipo (semelhante à programação de modelos em C ++), mas estou me perguntando se Haskell também pode parametrizar um tipo sobre valores - se ele suporta tipos dependentes. Com tipos dependentes, você pode ter um tipo parametrizado sobre números inteiros, por exemplo, vetores de tamanho n, matrizes de tamanho n × m, etc.
Se não, por que não? E existe alguma possibilidade de que seja suportado no futuro?
Haskell não possui totalmente tipos dependentes, embora possa se aproximar muito com extensões como DataKindse TypeFamilies. A questão no momento, até onde eu sei, é que o Haskell em nível de valor tem partes inferiores explícitas, mas o Haskell em nível de tipo não.
Isso não o impede de parametrizar tipos sobre outros tipos, incluindo o DataKindlevantamento de valores . A partir do GHC 7.6, e com DataKindsativado, você pode usar cordas e cordas de nível natural, bem como tuplas, listas de nível de tipo e elevações de nível de tipo de qualquer tipo (não generalizado, não generalizado) , sem restrição) tipos de dados algébricos, que são semelhantes à (mas muito mais geral que) a capacidade do C ++ de usar números inteiros em modelos.
Para expandir um pouco o que o Flame de Ptharien explicou bem sobre o status atual - e GHC Haskell parece estar se movendo mais na direção dos tipos dependentes (preservando a separação de fases) em cada versão.
Assim, por exemplo, no ICFP 2013, em setembro, deve ser apresentado um documento sobre a próxima fase deste processo, "Em direção a Haskell de tipo dependente: Sistema FC com igualdade de gênero" , sobre o colapso dos níveis de tipo e tipo. Como foi anunciado o plano há cerca de 3 anos .
E até menciona o próximo passo: "Também estamos cientes de que a dissertação de Adam Gundry incluirá tipos Π em uma versão do System FC e também queremos disponibilizar esse recurso no idioma de origem. (Comunicação pessoal)"
fonte
Tradicionalmente, Haskell tentou falsificá-lo, mas o resultado final é um sistema de tipos muito maior e aparentemente repetitivo. Mas isso pode mudar em breve! Vejo:
fonte