Теория гомоиконического типа - PullRequest
Новая
       45

Теория гомоиконического типа

10 голосов
/ 29 ноября 2011

Lisp обладает свойством быть homoiconic , то есть представление кода, используемого языковой реализацией (списками), также доступно и идиоматически используется программами, которые хотят представлять код для своих собственные цели.

Другое основное семейство функциональных языков программирования, ML, основано на теории типов, что означает, что языковая реализация требует более сложного представления кода, а также менее небрежно относится к тому, что вам разрешено делать, поэтому обычно внутреннее представление недоступно для программ. Например, средства проверки корректности для логики высшего порядка часто реализуются на языках семейства ML, но обычно реализуют свою собственную систему теории типов, фактически игнорируя тот факт, что компилятор ML уже имеет такую ​​систему.

Есть ли исключения из этого? Какие-нибудь языки программирования, основанные на теории типов, которые предоставляют представление своего кода для программного использования?

Ответы [ 5 ]

12 голосов
/ 29 ноября 2011

Взгляните на системы типов для поэтапного выполнения (слабая форма метапрограммирования), например, та, которая используется в языке MetaML.

Также отметим, что, хотя на первый взгляд привлекательный, гомойконичность (и метапрограммирование с помощью прямого манипулирования АСТ в целом) на практике оказалась неудобной. Взгляните на современные системы макросов в Nemerle и экспериментальное расширение Scala, которые, если я правильно помню, полагаются на квази-цитату.

Что касается того, почему теория типов ML не используется повторно, вот несколько соображений:

  • Система типов ML недостаточно выразительна (подумайте о зависимых типах)
  • Система типов ML загрязнена общей рекурсией и изменчивыми ссылками
  • Нет единого мнения о том, какая система типов может использоваться как для проверки, так и для написания программ общего назначения. Это постоянное исследование. См. Например http://www.nii.ac.jp/shonan/seminar007/. Поэтому каждый проверяющий реализует свою собственную теорию только потому, что авторы исправляют недостатки в предыдущих теориях типов.
7 голосов
/ 29 ноября 2011

Другое основное семейство функциональных языков программирования ... основано на теории типов, что означает, что языковая реализация требует более сложного представления кода

Я не вижу причин, почему это было бы правдой.

Если вы еще этого не видели, вас может заинтересовать Лискелл, который рекламирует себя как Haskell semantics + Lisp syntax.

3 голосов
/ 29 ноября 2011

Основная выгода от того, что Лисп гомоичен, - сильная способность метапрограммирования.Я думаю, вы могли бы взглянуть на метапрограммирование безопасного типа , в частности Template Haskell .

2 голосов
/ 08 сентября 2014

Шен :

Шен имеет одну из самых мощных систем типов в рамках функционального программирования.Шен работает по сокращенной инструкции Lisp и предназначен для переносимости.

Например: 

(define total
  {(list number) --> number}
  [] -> 0
  [X | Y] -> (+ X (total Y)))

Типизированная ракетка :

Typed Racket - это семейство языков, каждый из которых обязывает программы, написанные на этом языке, подчиняться системе типов, гарантирующей отсутствие многих распространенных ошибок.

Например: 

#lang typed/racket
(: sum-list (-> (Listof Number) Number))
(define (sum-list l)
  (cond [(null? l) 0]
        [else (+ (car l) (sum-list (cdr l)))]))

Mercury :

Mercury - это логический / функциональный язык программирования, который сочетает в себе ясность и выразительность декларативного программирования с расширенными функциями статического анализа и обнаружения ошибок.

Например: 

:- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).
1 голос
/ 10 августа 2015

Есть ли исключения из этого?Любые языки программирования, основанные на теории типов, которые предоставляют представление своего кода для программного использования?

SML не предоставляет программный код, а OCaml и F # делают.OCaml имеет полную систему макросов.

...