Учитывая, что моя работа сосредоточена на связанных вопросах области видимости и безопасности типов, кодируемых на уровне типов, я наткнулся на этот старый вопрос, пока гуглил, и подумал, что попробую.

Я думаю, этот пост дает ответ, довольно близкий к исходной спецификации. Все это получается на удивление коротким, если у вас есть правильная настройка.

Сначала я начну с примера программы, чтобы дать вам представление о том, как выглядит конечный результат:

program :: Program
program = Program
  $  Declare (Var :: Name "foo") (Of :: Type Int)
  :> Assign  (The (Var :: Name "foo")) (EInt 1)
  :> Declare (Var :: Name "bar") (Of :: Type Bool)
  :> increment (The (Var :: Name "foo"))
  :> Assign  (The (Var :: Name "bar")) (ENot $ EBool True)
  :> Done

Определение объема

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

GHC.TypeLits предоставляет нам строки уровня типа (называемые Symbol), поэтому мы можем очень хорошо использовать строки в качестве имен переменных, если захотим. И поскольку мы хотим обеспечить безопасность типов, каждое объявление переменной поставляется с аннотацией типа, которую мы будем хранить вместе с именем переменной. Таким образом, наш тип прицелов: [(Symbol, *)].

Мы можем использовать семейство типов, чтобы проверить, находится ли данный Symbol в области видимости, и вернуть связанный с ним тип, если это так:

type family HasSymbol (g :: [(Symbol,*)]) (s :: Symbol) :: Maybe * where
  HasSymbol '[]            s = 'Nothing
  HasSymbol ('(s, a) ': g) s = 'Just a
  HasSymbol ('(t, a) ': g) s = HasSymbol g s

Из этого определения мы можем определить понятие переменной: переменная типа a в области видимости g является символом s, так что HasSymbol g s возвращает 'Just a. Это то, что представляет собой тип данных ScopedSymbol, используя количественную оценку существования для хранения s.

data ScopedSymbol (g :: [(Symbol,*)]) (a :: *) = forall s.
  (HasSymbol g s ~ 'Just a) => The (Name s)

data Name (s :: Symbol) = Var

Здесь я целенаправленно злоупотребляю нотациями повсюду: The - конструктор для типа ScopedSymbol, а Name - _ 18_ с более приятным именем и конструктором. Это позволяет писать такие тонкости, как:

example :: ScopedSymbol ('("foo", Int) ': '("bar", Bool) ': '[]) Bool
example = The (Var :: Name "bar")

Заявления

Теперь, когда у нас есть понятие области видимости и хорошо типизированных переменных в этой области, мы можем начать рассматривать эффекты, которые должны иметь Statements. Учитывая, что новые переменные могут быть объявлены в Statement, нам нужно найти способ распространить эту информацию в области видимости. Ключевым моментом в ретроспективе является наличие двух индексов: входной и выходной области.

Чтобы Declare новая переменная вместе с ее типом расширила текущую область действия парой имени переменной и соответствующего типа.

Assignments, с другой стороны, не изменяют объем. Они просто связывают ScopedSymbol с выражением соответствующего типа.

data Statement (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
  Declare :: Name s -> Type a -> Statement g ('(s, a) ': g)
  Assign  :: ScopedSymbol g a -> Exp g a -> Statement g g

data Type (a :: *) = Of

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

example' :: Statement '[] ('("foo", Int) ': '[])
example' = Declare (Var :: Name "foo") (Of :: Type Int)

example'' :: Statement ('("foo", Int) ': '[]) ('("foo", Int) ': '[])
example'' = Assign (The (Var :: Name "foo")) (EInt 1)

Statements можно объединить в цепочку с сохранением области видимости путем определения следующего GADT последовательностей, выровненных по типу:

infixr 5 :>
data Statements (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
  Done :: Statements g g
  (:>) :: Statement g h -> Statements h i -> Statements g i

Выражения

Выражения в основном не изменились по сравнению с исходным определением, за исключением того, что теперь они имеют ограниченную область видимости, а новый конструктор EVar позволяет нам разыменовать ранее объявленную переменную (используя ScopedSymbol), давая нам выражение соответствующего типа.

data Exp (g :: [(Symbol,*)]) (t :: *) where
  EVar    :: ScopedSymbol g a -> Exp g a
  EBool   :: Bool -> Exp g Bool
  EInt    :: Int  -> Exp g Int
  EAdd    :: Exp g Int -> Exp g Int -> Exp g Int
  ENot    :: Exp g Bool -> Exp g Bool

Программ

Program - это просто последовательность операторов, начинающаяся в пустой области видимости. Мы снова используем экзистенциальную количественную оценку, чтобы скрыть объем, который мы получили.

data Program = forall h. Program (Statements '[] h)

Очевидно, что можно писать подпрограммы на Haskell и использовать их в своих программах. В этом примере у меня очень простой increment, который можно определить так:

increment :: ScopedSymbol g Int -> Statement g g
increment v = Assign v (EAdd (EVar v) (EInt 1))

Я загрузил весь фрагмент кода вместе с правильными LANGUAGE прагмами и примерами, перечисленными здесь в отдельном gist < / а>. Однако я не включил туда никаких комментариев.

Вы должны знать, что ваши цели довольно высоки. Я не думаю, что вы далеко продвинетесь, рассматривая свои переменные именно как строки. Я бы сделал что-нибудь более раздражающее, но более практичное. Определите монаду для вашего DSL, которую я назову M:

newtype M a = ...

data Exp a where
    ... as before ...

data Var a  -- a typed variable

assign :: Var a -> Exp a -> M ()
declare :: String -> a -> M (Var a)

Я не уверен, почему у вас Exp a для назначения и только a для объявления, но я воспроизвел это здесь. String в declare предназначен только для косметики, если он вам нужен для генерации кода или отчетов об ошибках или чего-то еще - идентификатор переменной действительно не должен быть привязан к этому имени. Так что обычно он используется как

myFunc = do
    foobar <- declare "foobar" 42

что является раздражающим избыточным битом. В Haskell нет подходящего способа обойти это (хотя в зависимости от того, что вы делаете со своим DSL, вам может вообще не понадобиться строка).

Что касается реализации, может быть что-то вроде

data Stmt = forall a. Assign (Var a) (Exp a)
          | forall a. Declare (Var a) a

data Var a = Var String Integer  -- string is auxiliary from before, integer
                                 -- stores real identity.

Для M нам нужен уникальный набор имен и список операторов для вывода.

newtype M a = M { runM :: WriterT [Stmt] (StateT Integer Identity a) }
    deriving (Functor, Applicative, Monad)

Тогда операции как обычно довольно тривиальные.

assign v a = M $ tell [Assign v a]

declare name a = M $ do
    ident <- lift get
    lift . put $! ident + 1
    let var = Var name ident
    tell [Declare var a]
    return var

Я сделал довольно большой DSL для генерации кода на другом языке, используя довольно похожий дизайн, и он хорошо масштабируется. Я считаю хорошей идеей оставаться «на земле», просто занимаясь твердотельным моделированием, не используя слишком много причудливых магических функций на уровне шрифтов и принимая незначительные лингвистические неудобства. Таким образом, главная сила Haskell - способность абстрагироваться - все еще может быть использована для кода в вашем DSL.

Одним из недостатков является то, что все должно быть определено в блоке do, что может стать препятствием для хорошей организации по мере роста объема кода. Я украду declare, чтобы показать способ обойти это:

declare :: String -> M a -> M a

используется как

foo = declare "foo" $ do
    -- actual function body

тогда ваш M может иметь в качестве компонента своего состояния кэш от имен до переменных, и в первый раз, когда вы используете объявление с определенным именем, вы его визуализируете и помещаете в переменную (для этого потребуется немного более изощренный моноид, чем [Stmt] в качестве цели вашего Writer). Позже вы просто посмотрите переменную. К сожалению, он имеет довольно гибкую зависимость от уникальности имен; явная модель пространств имен может помочь в этом, но никогда не устраняет ее полностью.

Увидев весь код @Cactus и предложения Haskell @luqui, мне удалось получить решение, близкое к тому, что я хочу в Идрисе. Полный код доступен по следующей сути:

(https://gist.github.com/rodrigogribeiro/33356c62e36bff54831d)

Некоторые мелочи, которые мне нужно исправить в предыдущем решении:

1. Я не знаю (пока), поддерживает ли Идрис перегрузку целочисленных букв, что было бы весьма полезно для построения моего DSL.
2. Я попытался определить в синтаксисе DSL оператор префикса для переменных программы, но он работал не так, как мне хотелось бы. У меня есть решение (в предыдущем разделе), которое использует ключевое слово --- use --- для доступа к переменной.

Я уточню эти мелкие моменты с парнями на канале Idris #freenode, чтобы узнать, возможны ли эти два момента.