Deve um idioma que implementa Monads ser digitado estaticamente?

StackOverflow https://stackoverflow.com/questions/394709

Pergunta

Estou aprendendo estilo de programação funcional. Em não temem as Mônadas , Brian Beckman deu uma introdução brilhante sobre Monad. Ele mencionou que Monad é sobre composição de funções, de modo a complexidade endereço.

Um Mônada inclui uma função unit que as transferências de tipo T para um tipo amplificado H (T); e uma função de ligação que, dada a função de T para M (L), transformações do tipo M (t) para outro tipo M (L). (U pode ser T, mas não é necessariamente).

No meu entendimento, a Mônada linguagem de execução devem ser estaticamente verificado tipo. Caso contrário, erros de tipo não pode ser encontrado durante a compilação e "complexidade" não é controlado. É meu entendimento correto?

Foi útil?

Solução

Existem muitas implementações de mônadas em linguagens com tipagem dinâmica:

Em geral, a Church-Turing-Tese diz-nos que tudo o que pode ser feito em um linguagem pode também ser feito em todos os outros Idioma.

Como você provavelmente pode dizer a partir da selecção de exemplos acima, eu sou (principalmente) um programador Ruby. Assim, apenas como uma brincadeira, peguei um dos exemplos acima e re-implementou em uma língua que eu sei absolutamente nada sobre, que é geralmente considerado como uma linguagem não muito poderoso, e que parece ser a única linguagem de programação no planeta para o qual eu não era capaz de encontrar um tutorial Mônada. Posso apresentar a você ... a Mônada Identidade em PHP: 

<?php
class Identity {
  protected $val;
  public function __construct($val) { $this->val = $val; }
  public static function m_return($a) { return new Identity($a); }
  public static function m_bind($id_a, $f) { return $f($id_a->val); }
}

var_dump(Identity::m_bind(
  Identity::m_return(1), function ($x) {
    return Identity::m_return($x+1);
  }
));
?>

Nenhum tipo estático, há genéricos, há fechamentos necessários.

Agora, se você realmente quiser verificar estaticamente mônadas, então você precisa de um sistema de tipo estático. Mas isso é mais ou menos uma tautologia: se você quiser verificar estaticamente tipos, você precisa de um verificador de tipo estático. Duh.

Com relação à sua pergunta:

No meu entendimento, a Mônada linguagem de execução devem ser estaticamente verificado tipo. Caso contrário, erros de tipo não pode ser encontrado durante a compilação e "complexidade" não é controlado. É meu entendimento correto?

Você está certo, mas isso não tem nada a ver com mônadas. Este é apenas sobre a verificação de tipo estático em geral, e se aplica igualmente bem para matrizes, listas ou inteiros chato mesmo simples.

Há também um arenque vermelho aqui: se você olhar, por exemplo, em implementações mônada em C #, Java ou C, eles são muito mais tempo e muito mais complexo do que, digamos, o exemplo PHP acima. Em particular, há toneladas de tipos em todos os lugares, por isso certamente aparência impressionante. Mas a verdade nua e crua é: 's sistemas do tipo de C C #, Java de e não são realmente poderoso o suficiente para expressar o tipo de Monad. Em particular, é um tipo Monad polimórfica rank-2, mas C # e Java único apoio rank-1 Polymorfismo (que eles chamam de "genéricos", mas é a mesma coisa) e C não apoiar nem isso.

Assim, mônadas são, de facto, não estaticamente Type-check-in C #, Java e C. (que é, por exemplo, a razão pela qual o compreensões LINQ mônada são definidos como um padrão e não como um tipo: porque você simplesmente não pode expressar do tipo em C #.) Todo o sistema de tipo estático faz, é tornar a implementação muito mais complexa, sem realmente ajudando. Ele requer um sistema de tipo muito mais sofisticado, como Haskell de, para obter tipo de segurança real para mônadas.

Nota: o que eu escrevi acima única se aplica ao próprio tipo monad genérico, como @Porges ressalta. Você também pode se expressar o tipo de qualquer específica mônada, como List ou Maybe, mas você não pode expressar o tipo de si Monad. E-check digite Isso significa que você não pode o fato de que "List IS-A Monad", e você não pode escrever-verifique as operações genéricos que o trabalho em todas as instâncias do Monad.

(Note-se que a verificação de que Monad também obedece a Mônada leis , além de conformidade com a Mônada tipo é provavelmente demasiado, mesmo para sistema do tipo de Haskell. Você provavelmente precisa tipos dependentes e talvez até um provador de teoremas automático full-blown para isso.)

Outras dicas

Não é certamente o caso de que uma linguagem monads execução deve ser tipagem estática, como o seu título da pergunta pede. Pode ser uma boa idéia, pelas razões que você esboço, mas os erros deixando de ser detectados em tempo de compilação nunca deixou ninguém. Basta olhar para quantas pessoas escrevem PHP.

Você precisa de tampas para a Mônada Estado. Eu olhei para cima, PHP tem encerramentos desde 5.3. Então, isso não seria um problema.

Não, em php não é possível implementar mônadas. Você precisa de tampas para isso. Nunca a menos, o conceito de Talvez pode ser ainda útil, quando você simular padrão de correspondência com classes: 

abstract class Maybe {
        abstract public function isJust();
        public function isNothing(){
                return !$this->isJust();
        }
}

class Just extends Maybe {
        protected $val = null;
        public function __construct($val){
                $this->val = $val;

        }
        public function isJust(){
                return true;
        }
        public function getVal(){
                return $this->val;
        }

}
class Nothing extends Maybe {
        protected $val = null;
        public function __construct(){

        }
        public function isJust(){
                return false;
        }
}

function just(){
        print "isJust";
}
function nothing(){
        print "nothing";
}
function MaybeFunc(Maybe $arg){
        if(get_class($arg) == 'Just'){
                print "Just";
        } else {
                print "Nothing";
        }
}

MaybeFunc(new Just(5));
MaybeFunc(new Nothing());
Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top