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

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

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

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

Источник

5 ответов

Решение

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

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

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

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

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

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

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

Источник

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

Источник

Шен:

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

Например:

:- func sum(list(int)) = int.   
sum([]) = 0.
sum([X|Xs]) = X + sum(Xs).
Источник

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

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

Источник
Другие вопросы по тегам