Início / coding / Perguntas / 77266525
Accepted
Michael Litchard
Asked: 2023-10-10 22:06:30 +0800 CST

Alguém poderia fornecer um exemplo do que a função `weaken` faria?

  • 772

No Thinking With TypesExercício 11.2-i é escrever a função com a seguinte assinatura de tipo.

weaken :: OpenSum f ts -> OpenSum f (x ': ts)

data OpenSum (f :: k -> Type) (ts :: [k]) where
  UnsafeOpenSum :: Int -> f t -> OpenSum f ts

Acredito que o parágrafo anterior ao exercício forneça contexto suficiente para saber o que essa função realiza, mas não está claro para mim.

Na prática, também é útil poder ampliar as possibilidades de um montante em aberto. Uma nova função, enfraquecer, alinha o tipo machado na frente da lista de possibilidades.

Se eu tivesse alguns exemplos de uso dessa função, seria uma grande ajuda para eu concluir este exercício.

haskell

1 respostas

  1. Best Answer

    Na UnsafeOpenSum :: Int -> f t -> OpenSum f tslista tsnão há nenhuma relação com as outras variáveis ​​de tipo, portanto este construtor pode produzir valores do tipo OpenSum f tspara qualquer ts.

    Portanto, obtemos

    weaken :: OpenSum f ts -> OpenSum f (x ': ts)
weaken (UnsafeOpenSum i ft) = UnsafeOpenSum newI ft
   where newI = ...  -- To do

    Observe que os dois termos UnsafeOpenSum i ftparecem iguais (exceto pela iparte), mas são de tipos distintos.

    Além disso, precisamos de um novo índice newI, que você possa calcular em termos de i.

    weaken (UnsafeOpenSum i ft) = UnsafeOpenSum newI ft
       \- :: OpenSum f ts     |
                              \- :: OpenSum f (x :' ts)

    Como ter acesso ao construtor permite escolher qualquer lista tsdo tipo, o construtor é nomeado Unsafe....para lembrar aos usuários que deve-se usá-lo apenas para implementar primitivas seguras (como weaken). Depois disso, espera-se que os usuários usem as primitivas seguras sem acessar o construtor de nível inferior.

    • 4

relate perguntas