Posso imprimir em Haskell o tipo de função polimórfica como seria se eu passasse a ela uma entidade de um tipo concreto?

Dec 12 2020

Aqui está uma função polimórfica em 3 tipos:

:t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c

e aqui uma função não polimórfica:

:t Data.Char.digitToInt
Data.Char.digitToInt :: Char -> Int

Se aplicarmos o primeiro ao último, obteremos uma função polimórfica em 1 tipo:

:t (.) Data.Char.digitToInt
(.) Data.Char.digitToInt :: (a -> Char) -> a -> Int

o que significa que (.)foi "instanciado" (não tenho certeza se este é o termo correto; como um programador C ++, eu chamaria assim) com b === Chare c === Int, então a assinatura do (.)que é aplicada digitToInté a seguinte

(Char -> Int) -> (a -> Char) -> a -> Int

Minha pergunta é: existe uma maneira de ter essa assinatura impressa na tela, dada (.), digitToInte a "informação" que desejo aplicar a primeira à segunda?

Para os interessados, esta questão foi anteriormente encerrada como duplicado desta .

Respostas

7 MikeSpivey Dec 13 2020 at 06:32

Outras respostas requerem a ajuda de funções que foram definidas com tipos artificialmente restritos, como a asTypeOffunção na resposta do HTNW. Isso não é necessário, como mostra a seguinte interação:

Prelude> let asAppliedTo f x = const f (f x)

Prelude> :t head `asAppliedTo` "x"
head `asAppliedTo` "x" :: [Char] -> Char

Prelude> :t (.) `asAppliedTo` Data.Char.digitToInt
(.) `asAppliedTo` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Isso explora a falta de polimorfismo na ligação lambda que está implícita na definição de asAppliedTo. Ambas as ocorrências de fem seu corpo devem ser do mesmo tipo, e esse é o tipo de seu resultado. A função constusada aqui também tem seu tipo natural a -> b -> a:

const x y = x
12 HTNW Dec 12 2020 at 09:09

Existe esta pequena função elegante escondida em um canto do Prelude:

Prelude.asTypeOf :: a -> a -> a
asTypeOf x _ = x

Está documentado como "forçando seu primeiro argumento a ter o mesmo tipo do segundo." Podemos usar isso para forçar o tipo do (.)primeiro argumento de:

-- (.) = \x -> (.) x = \x -> (.) $ x `asTypeOf` Data.Char.digitToInt -- eta expansion followed by definition of asTypeOf -- the RHS is just (.), but restricted to arguments with the same type as digitToInt -- "what is the type of (.) when the first argument is (of the same type as) digitToInt?" ghci> :t \x -> (.) $ x `asTypeOf` Data.Char.digitToInt
\x -> (.) $ x `asTypeOf` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Claro, isso funciona para quantos argumentos você precisar.

ghci> :t \x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
\x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
  :: (Char -> Int) -> ([Char] -> Char) -> [Char] -> Int

Você pode considerar isso uma variação da ideia de @KABuhr nos comentários - usando uma função com uma assinatura mais restritiva do que sua implementação para orientar a inferência de tipo - exceto que não temos que definir nada nós mesmos, ao custo de não sermos capazes de apenas copie a expressão em questão sob um lambda.

8 K.A.Buhr Dec 12 2020 at 09:57

Acho que a resposta de @ HTNW provavelmente cobre isso, mas para completar, veja como a inContextsolução funciona em detalhes.

A assinatura de tipo da função:

inContext :: a -> (a -> b) -> a

significa que, se você tem algo que deseja digitar e um "contexto" no qual é usado (expressável como um lambda que o considera como um argumento), diga com tipos:

thing :: a1
context :: a2 -> b

Você pode forçar a unificação de a1(o tipo geral de thing) com a2(as restrições do contexto) simplesmente construindo a expressão:

thing `inContext` context

Normalmente, o tipo unificado thing :: aseria perdido, mas a assinatura de tipo de inContextimplica que o tipo de toda essa expressão resultante também será unificado com o tipo desejado a, e GHCi felizmente informará o tipo dessa expressão.

Portanto, a expressão:

(.) `inContext` \hole -> hole digitToInt

acaba sendo atribuído o tipo que (.)teria dentro do contexto especificado. Você pode escrever isso, de forma um tanto enganosa, como:

(.) `inContext` \(.) -> (.) digitToInt

uma vez que (.)é um nome de argumento tão bom para um lambda anônimo quanto holeé. Isso é potencialmente confuso, já que estamos criando uma ligação local que obscurece a definição de nível superior de (.), mas ainda está nomeando a mesma coisa (com um tipo refinado), e esse abuso de lambdas nos permitiu escrever a expressão original (.) digitToIntliteralmente, com o clichê apropriado.

Na verdade, é irrelevante como inContexté definido, se você estiver apenas pedindo ao GHCi seu tipo, então inContext = undefinedteria funcionado. Mas, apenas olhando para a assinatura de tipo, é fácil dar inContextuma definição de trabalho:

inContext :: a -> (a -> b) -> a
inContext a _ = a

Acontece que essa é apenas a definição de const, então inContext = constfunciona também.

Você pode usar inContextpara digitar várias coisas de uma vez, e elas podem ser expressões em vez de nomes. Para acomodar o primeiro, você pode usar tuplas; para que o último funcione, você deve usar nomes de argumento mais sensatos em seus lambas.

Então, por exemplo:

λ> :t (fromJust, fmap length) `inContext` \(a,b) -> a . b
(fromJust, fmap length) `inContext` \(a,b) -> a . b
  :: Foldable t => (Maybe Int -> Int, Maybe (t a) -> Maybe Int)

informa que, na expressão fromJust . fmap length, os tipos foram especializados para:

fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int
6 FyodorSoikin Dec 12 2020 at 03:35

Você pode fazer isso usando a TypeApplicationsextensão, que permite especificar explicitamente quais tipos deseja usar para instanciar os parâmetros de tipo:

λ :set -XTypeApplications                                 
λ :t (.) @Char @Int
(.) @Char @Int :: (Char -> Int) -> (a -> Char) -> a -> Int

Observe que os argumentos devem estar na ordem exata.

Para funções que possuem uma assinatura de tipo "regular" como foo :: a -> b, a ordem é definida pela ordem em que os parâmetros de tipo aparecem pela primeira vez na assinatura.

Para funções que usam ExplicitForalllike foo :: forall b a. a -> b, a ordem é definida pelo que quer que esteja forall.


Se você quiser descobrir o tipo especificamente baseado na aplicação (.)de digitToChar(em oposição a apenas saber que tipos de preencher), eu tenho certeza que você não pode, em GHCi, mas recomendo apoio Haskell IDE.

Por exemplo, é assim que parece para mim no VSCode (aqui está a extensão ):

5 chi Dec 12 2020 at 16:39

Esta é uma variação menor da resposta do HTNW.

Suponha que temos qualquer expressão potencialmente grande envolvendo um identificador polimórfico poly

 .... poly ....

e nos perguntamos como o tipo polimórfico foi instanciado naquele ponto.

Isso pode ser feito explorando dois recursos do GHC: asTypeOf(conforme mencionado pelo HTNW) e orifícios digitados , da seguinte forma:

 .... (poly `asTypeOf` _) ....

Ao ler o _furo, o GHC irá gerar um erro informando o tipo de termo que deve ser inserido no lugar daquele furo. Desde que usamos asTypeOf, isso deve ser o mesmo que o tipo da instância particular de polyque precisamos naquele contexto.

Aqui está um exemplo em GHCi:

> ((.) `asTypeOf` _) Data.Char.digitToInt
<interactive>:11:17: error:
    * Found hole: _ :: (Char -> Int) -> (a -> Char) -> a -> Int