Esclarecimento sobre tipos existenciais em Haskell

Estou tentando entender os tipos existentes em Haskell e me deparei com um PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf

Corrija meus entendimentos abaixo que tenho até agora.

• Tipos existentes não parecem estar interessados ​​no tipo que eles contêm, mas os padrões correspondentes dizem que existe algum tipo que não sabemos qual é o tipo até & a menos que usemos Typeable ou Data.
• Nós os usamos quando queremos ocultar tipos (por exemplo, para listas heterogêneas) ou realmente não sabemos quais são os tipos em tempo de compilação.
• GADT's fornecer a sintaxe clara e melhor para código usando tipos existenciais, fornecendo implícitas forall' s

Minhas Dúvidas

• Na página 20 do PDF acima, é mencionado no código abaixo que é impossível para uma Função exigir Buffer específico. Por que é tão? Quando estou escrevendo uma Função, sei exatamente que tipo de buffer vou usar, mesmo que eu não saiba quais dados serão inseridos. O que há de errado em Ter :: Worker MemoryBuffer IntSe eles realmente querem abstrair sobre o Buffer, eles podem ter um tipo Sum data Buffer = MemoryBuffer | NetBuffer | RandomBuffere um tipo como:: Worker Buffer Int

data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

• Como Haskell é uma linguagem de apagamento de tipo completo como C, então Como ele sabe, em tempo de execução, qual função chamar. É algo como manteremos poucas informações e repassarmos uma enorme V-Table of Functions e, em tempo de execução, descobriremos a partir da V-Table? Se for assim, que tipo de informação será armazenada?

Os GADTs fornecem a sintaxe clara e melhor para codificar usando Tipos Existenciais, fornecendo

Eu acho que há um consenso geral de que a sintaxe do GADT é melhor. Eu não diria que é porque os GADTs fornecem formas implícitas, mas sim porque a sintaxe original, ativada com a ExistentialQuantificationextensão, é potencialmente confusa / enganosa. Essa sintaxe, é claro, se parece com:

data SomeType = forall a. SomeType a

ou com uma restrição:

data SomeShowableType = forall a. Show a => SomeShowableType a

e acho que o consenso é que o uso da palavra-chave forallaqui permite que o tipo seja facilmente confundido com o tipo completamente diferente:

data AnyType = AnyType (forall a. a)    -- need RankNTypes extension

Uma sintaxe melhor pode ter usado uma existspalavra-chave separada , então você deve escrever:

data SomeType = SomeType (exists a. a)   -- not valid GHC syntax

A sintaxe do GADT, usada com implícita ou explícita forall, é mais uniforme entre esses tipos e parece ser mais fácil de entender. Mesmo com um explícito forall, a seguinte definição transmite a ideia de que você pode pegar um valor de qualquer tipo ae colocá-lo dentro de um monomórfico SomeType':

data SomeType' where
    SomeType' :: forall a. (a -> SomeType')   -- parentheses optional

e é fácil ver e entender a diferença entre esse tipo e:

data AnyType' where
    AnyType' :: (forall a. a) -> AnyType'

Tipos existentes não parecem estar interessados ​​no tipo que eles contêm, mas os padrões correspondentes dizem que existe algum tipo que não sabemos qual é o tipo até & a menos que usemos Typeable ou Data.

Nós os usamos quando queremos ocultar tipos (por exemplo, para listas heterogêneas) ou realmente não sabemos quais são os tipos em tempo de compilação.

Eu acho que eles não estão muito longe, embora você não precise usar Typeableou Datausar tipos existenciais. Eu acho que seria mais preciso dizer que um tipo existencial fornece uma "caixa" bem digitada em torno de um tipo não especificado. A caixa "oculta" o tipo em um sentido, o que permite fazer uma lista heterogênea dessas caixas, ignorando os tipos que elas contêm. Acontece que um existencial irrestrito, como SomeType'acima, é bastante inútil, mas um tipo restrito:

data SomeShowableType' where
    SomeShowableType' :: forall a. (Show a) => a -> SomeShowableType'

permite padronizar a correspondência para espiar dentro da "caixa" e disponibilizar as facilidades da classe de tipo:

showIt :: SomeShowableType' -> String
showIt (SomeShowableType' x) = show x

Observe que isso funciona para qualquer classe de tipo, não apenas Typeableou Data.

Com relação à sua confusão sobre a página 20 do deck de slides, o autor está dizendo que é impossível para uma função que exista um existencial Worker exigir uma instância Workerespecífica Buffer. Você pode escrever uma função para criar uma Workerusando um tipo específico de Buffer, como MemoryBuffer:

class Buffer b where
  output :: String -> b -> IO ()
data Worker x = forall b. Buffer b => Worker {buffer :: b, input :: x}
data MemoryBuffer = MemoryBuffer
instance Buffer MemoryBuffer

memoryWorker = Worker MemoryBuffer (1 :: Int)
memoryWorker :: Worker Int

mas se você escrever uma função que usa um Workerargumento as, ela poderá usar apenas os Bufferrecursos da classe de tipo geral (por exemplo, a função output):

doWork :: Worker Int -> IO ()
doWork (Worker b x) = output (show x) b

Ele não pode tentar exigir que bseja um tipo específico de buffer, mesmo através da correspondência de padrões:

doWorkBroken :: Worker Int -> IO ()
doWorkBroken (Worker b x) = case b of
  MemoryBuffer -> error "try this"       -- type error
  _            -> error "try that"

Por fim, informações de tempo de execução sobre tipos existenciais são disponibilizadas por meio de argumentos implícitos de "dicionário" para as classes de tipos envolvidas. O Workertipo acima, além de ter campos para o buffer e a entrada, também possui um campo implícito invisível que aponta para o Bufferdicionário (um pouco como a tabela v, embora seja dificilmente enorme, pois contém apenas um ponteiro para a outputfunção apropriada ).

Internamente, a classe de tipo Bufferé representada como um tipo de dados com campos de função e as instâncias são "dicionários" desse tipo:

data Buffer' b = Buffer' { output' :: String -> b -> IO () }

dBuffer_MemoryBuffer :: Buffer' MemoryBuffer
dBuffer_MemoryBuffer = Buffer' { output' = undefined }

O tipo existencial possui um campo oculto para este dicionário:

data Worker' x = forall b. Worker' { dBuffer :: Buffer' b, buffer' :: b, input' :: x }

e uma função como doWorkessa opera em Worker'valores existenciais é implementada como:

doWork' :: Worker' Int -> IO ()
doWork' (Worker' dBuf b x) = output' dBuf (show x) b

Para uma classe de tipo com apenas uma função, o dicionário é realmente otimizado para um novo tipo; portanto, neste exemplo, o Workertipo existencial inclui um campo oculto que consiste em um ponteiro de função para a outputfunção do buffer e essa é a única informação de tempo de execução necessária por doWork.

Na página 20 do PDF acima, é mencionado no código abaixo que é impossível para uma Função exigir Buffer específico. Por que é tão?

Como Worker, conforme definido, leva apenas um argumento, o tipo do campo "entrada" (variável de tipo x). Por exemplo, Worker Inté um tipo. A variável type b, em vez disso, não é um parâmetro de Worker, mas é uma espécie de "variável local", por assim dizer. Não pode ser passado como em Worker Int String- isso provocaria um erro de tipo.

Se, em vez disso, definimos:

data Worker x b = Worker {buffer :: b, input :: x}

então Worker Int Stringfuncionaria, mas o tipo não é mais existencial - agora sempre precisamos passar também o tipo de buffer.

Como Haskell é uma linguagem de apagamento de tipo completo como C, então Como ele sabe, em tempo de execução, qual função chamar. É algo como manteremos poucas informações e repassarmos uma enorme V-Table of Functions e, em tempo de execução, descobriremos a partir da V-Table? Se for assim, que tipo de informação será armazenada?

Isso está aproximadamente correto. Resumidamente, toda vez que você aplica o construtor Worker, o GHC deduz o btipo dos argumentos de Workere depois procura uma instância Buffer b. Se isso for encontrado, o GHC inclui um ponteiro adicional para a instância no objeto. Na sua forma mais simples, isso não é muito diferente do "ponteiro para a tabela" que é adicionado a cada objeto no OOP quando funções virtuais estão presentes.

No caso geral, pode ser muito mais complexo. O compilador pode usar uma representação diferente e adicionar mais ponteiros em vez de um único (por exemplo, adicionar diretamente os ponteiros a todos os métodos de instância), se isso acelerar o código. Além disso, às vezes o compilador precisa usar várias instâncias para satisfazer uma restrição. Por exemplo, se precisamos armazenar a instância para Eq [Int]... então não há uma, mas duas: uma para Inte uma para listas, e as duas precisam ser combinadas (em tempo de execução, exceto otimizações).

É difícil adivinhar exatamente o que o GHC faz em cada caso: isso depende de uma tonelada de otimizações que podem ou não ser desencadeadas.

Você pode tentar pesquisar na implementação "baseada em dicionário" das classes de tipos para ver mais sobre o que está acontecendo. Você também pode pedir ao GHC para imprimir o Core otimizado interno -ddump-simple observar os dicionários que estão sendo construídos, armazenados e distribuídos. Preciso avisá-lo: o núcleo é de nível bastante baixo e pode ser difícil de ler a princípio.