Oi Habr.
Outro dia, em um dos meus projetos de hobby, surgiu a tarefa de escrever um repositório de métricas.
A tarefa em si é resolvida com muita simplicidade, mas meu problema com o Haskell (especialmente em projetos para meu próprio entretenimento) é que é impossível apenas pegar e resolver o problema. É necessário decidir, expandir, abstrair, abstrair e expandir ainda mais. Portanto, eu queria tornar o armazenamento de métricas extensível para não especificar antecipadamente o que elas estariam lá. Isso por si só é um tópico para um artigo separado, e hoje consideraremos um pequeno ingrediente: escrever um invólucro seguro para tipos anteriormente desconhecidos. Algo como digitação dinâmica, mas com garantias estáticas de que não faremos bobagens.
Acho que o artigo não abrirá nada de novo para os haskelistas experientes, mas agora vamos pelo menos colocar esse ingrediente fora da caixa e não seremos distraídos nos artigos subsequentes. Bem, ou você pode não ser tão modesto e dizer que eu já criei um padrão de design completo.
Então, primeiro formulamos o problema. Precisamos ser capazes de associar alguns objetos a valores de tipos anteriormente desconhecidos. Ou, em outras palavras, é necessário que os valores de tipos anteriormente desconhecidos atuem como chaves em algum tipo de mapa.
Naturalmente, não somos loucos e não precisaremos do apoio de valores de qualquer tipo. Exigimos que o tipo (mesmo que desconhecido) suporte a comparação no sentido de pedido. Em termos de Haskell, isso significa que apoiamos os tipos a que implementam a classe Ord a .
Observe que poderíamos exigir suporte para pegar um hash e verificar a igualdade, mas por vários motivos, seria mais conveniente e claro nos limitarmos à comparação.
Quando se trata de armazenar valores conhecidos por implementar algum tipo de classe, os tipos existenciais são geralmente usados no Haskell:
data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd
Portanto, se SomeOrd um objeto do tipo SomeOrd e fizermos a correspondência de padrões para ele:
foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ...
então, no ponto (1) , não sabemos qual o tipo val , mas sabemos (e, mais importante, o cronômetro também sabe) que val implementa a classe de tempo Ord .
No entanto, se as funções de tipo da classe implicarem dois (ou mais) argumentos, o uso desse registro será de pouca utilidade:
tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ?
Para usar os métodos Ord , é necessário que val e val2 mesmo tipo, mas isso não precisa ser feito! Acontece que nosso SomeOrd inútil. O que fazer?
Apesar do Haskell ser uma linguagem compilada com apagamento agressivo do tipo (após a compilação, eles geralmente não existem), o compilador ainda pode gerar representantes do tipo em tempo de execução, se perguntado sobre isso. A função representativa do tipo a é o valor do tipo TypeRep a e pedido geração é respondida por Typeclass Typeable .
By the wayA propósito, a não precisa ser um tipo no sentido usual, isto é, pertencer a uma variedade * . Pode ser qualquer outro tipo de k , que teoricamente permite que você faça coisas legais ao armazenar representantes em tempo de execução dos tipos aprendidos e similares, mas não descobri exatamente o que.
Além disso, se tivermos duas instâncias diferentes de rep1 :: TypeRep a, rep2 :: TypeRep b , podemos compará-las e verificar se elas representam o mesmo tipo ou não. Além disso, se eles realmente representam o mesmo tipo, então obviamente a coincide com b . E, o mais importante, a função de verificar representações de tipo quanto à igualdade retorna um resultado que pode convencer o digitador disso:
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
Que absurdo está escrito aqui?
Primeiro, eqTypeRep é uma função.
Em segundo lugar, é polimórfico, mas não apenas por tipo, mas também por variedades desses tipos. Isso é indicado pela parte de todos os forall k1 k2 (a :: k1) (b :: k2) - isso significa que b podem ser não apenas tipos comuns como Int ou [String] , mas também, por exemplo, construtores notórios (consulte DataKinds e outras tentativas de certificação Haskell). Mas não precisamos de tudo isso.
Terceiro, ele aceita duas representações de tempo de execução de tipos potencialmente diferentes, TypeRep a e TypeRep b .
Quarto, ele retorna um valor do tipo Maybe (a :~~: b) . A coisa mais interessante acontece aqui.
Se os tipos não corresponderem, a função retornará o habitual Nothing e tudo estará bem. Se os tipos corresponderem, a função retornará Just val , onde val é do tipo a :~~: b . Vamos ver que tipo é:
Agora vamos conversar. Suponha que obtemos um valor val do tipo a :~~: b . Como poderia ser construído? A única maneira é com o construtor HRefl , e esse construtor exige que nos dois lados do ícone :~~: seja o mesmo. Portanto, a coincide com b . Além disso, se zapternnom-match em val , o taypcheker também saberá. Portanto, sim, a função eqTypeRep retorna a prova de que dois tipos potencialmente diferentes são iguais se forem realmente iguais.
No entanto, no parágrafo acima, eu menti. Ninguém está nos impedindo de escrever em Haskell algo como
wrong :: Int :~~: String wrong = wrong
ou
wrong :: Int :~~: String wrong = undefined
ou quebre o sistema de várias maneiras menos óbvias. Esta é uma das manifestações do conhecido em círculos estreitos, dizendo que o Haskell é inconsistente como lógica. Em idiomas com sistemas de tipos mais fortes, essas definições não são carimbadas.
É por isso que, na parte da documentação citada acima, o valor final é mencionado. Ambas as variantes da implementação do wrong acima não produzem esse valor final, o que nos dá um pouco de razão e confiança: se o nosso programa no Haskell foi encerrado (e não ficou undefined ), então o resultado corresponde aos tipos escritos. Aqui, no entanto, existem alguns detalhes relacionados à preguiça, mas não abriremos este tópico.
E, a propósito, a segunda manifestação da fraqueza de Haskell no código acima é o tipo da função eqTypeRep . Em idiomas mais fortes, retornaria um valor de um tipo mais forte, que não apenas provaria a igualdade dos tipos se eles forem realmente iguais, mas também provaria sua desigualdade se eles forem realmente desiguais. A inconsistência da lógica de Haskell, no entanto, torna essas funções um pouco inúteis: tudo é importante quando você usa a linguagem como provador de teoremas, e não como linguagem de programação, e não usa Haskell como provador.
Bem, chega de teoria do log e do tipo, vamos voltar às nossas métricas. Agora basta desenhar uma coruja A discussão acima sugere que é suficiente armazenar em nosso tipo existencial também esta é a representação mais runtime do tipo, e tudo ficará bem.
Isso nos leva à seguinte implementação do nosso tipo de wrapper:
data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val
Agora, escrevemos uma função que aceita o seguinte:
- dois valores do tipo
Dyn ; - uma função que produz algo para dois valores de qualquer tipo ,
com base apenas nas constantes mencionadas ao criar o Dyn (o forall é responsável por isso),
e que é chamado se os dois Dyn armazenam valores do mesmo tipo; - e a função de fallback, que é chamada em vez da anterior, se os tipos ainda forem diferentes:
withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
SomeTypeRep é um wrapper existencial sobre TypeRep a para qualquer a .
Agora podemos implementar, por exemplo, verificação e comparação de igualdade:
instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare
Aqui aproveitamos o fato de que SomeTypeRep pode ser comparado entre si, portanto a função de fallback para pedidos também é compare .
Feito.
Só que agora é pecado não generalizar: observe que dentro de Dyn , toDyn , com withDyns não usamos Ord especificamente, e este pode ser qualquer outro conjunto de constantes, para que possamos ativar a extensão ConstraintKinds e generalizar , parametrizando Dyn conjunto específico de restrições que necessário em nossa tarefa específica:
data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
Então Dyn Ord será nosso tipo de Dyn Monoid e, digamos, Dyn Monoid permitirá que você armazene monoides arbitrários e faça algo monoidal com eles.
Vamos escrever as instâncias que precisamos para o nosso novo Dyn :
instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare
... apenas isso não funciona. O tipógrafo não sabe que Dyn Ord também implementa Eq ,
portanto, você deve copiar toda a hierarquia:
instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare
Bem, agora com certeza.
... talvez, em um Haskell moderno, você possa fazê-lo para que o próprio cronômetro exiba instâncias do formulário
instance C_i (Dyn (C_1, ... C_n)) where ...
porque há algo de prólogo, mas ainda não o fiz, vou ter que ficar sentado escolhendo isso. Fique atento.
E também, se você apertar os olhos com cuidado, poderá ver que nosso Dyn parece suspeito como um par dependente do tipo (ty : Type ** val : ty) das linguagens enigmáticas. Mas apenas em idiomas conhecidos por mim é impossível corresponder ao tipo, porque a parametridade (que neste caso, IMHO, é interpretada muito amplamente), mas aqui parece possível.
Mas a coisa mais importante - agora você pode seguramente ter algo como Map (Dyn Ord) SomeValue e usar quaisquer valores como chaves, desde que eles próprios suportem comparação. Por exemplo, identificadores com descrições de métricas podem ser usados como chaves, mas este é um tópico para o próximo artigo.