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

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

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

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

Ответ 1

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

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

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

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

Ответ 2

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

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

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

Ответ 3

Основная прибыль от Lisp, являющаяся homoiconic, является сильной способностью метапрограммирования. Я думаю, вы можете взглянуть на метапрограммирование, безопасное для типов, особенно Template Haskell.

Ответ 4

Shen:

У Shen есть одна из самых мощных систем типов в функциональном программировании. Шен работает под сокращенной инструкцией 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).

Ответ 5

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

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