Проверка корректности программы с использованием фантомных типов в Haskell

Question

Предположим, я работаю с кодом стековой машины, которая может выполнять некоторые простые операции (push constant, add, mul, dup, swap, pop, convert types) над целыми числами и удвоениями.

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

Я подозреваю, что можно использовать средство проверки типов Haskell для устранения некоторых ошибок, например:

• выскакивает из пустой стопки
• умножение удваивается с помощью умножения int

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

dup :: Stack (a :%: b) -> Stack (a :%: b :%: b)
int2double :: Stack (a :%: SInt) -> Stack (a :%: SDouble)

и так далее.Но тогда я не знаю, как сгенерировать код и вычислить размер стека.

Возможно ли это сделать вот так?И будет ли это просто / удобно / того стоит?

Answer 1

См. «Методы внедрения языков постфикса в Хаскелл» Криса Окасаки: http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#hw02

Кроме того, это:

{-# LANGUAGE TypeOperators #-}
module Stacks where

data a :* b = a :* b deriving Show
data NilStack = NilStack deriving Show

infixr 1 :*

class Stack a where
    stackSize :: a -> Int

instance Stack b => Stack (a :* b) where
    stackSize (_ :* x) = 1 + stackSize x

instance Stack NilStack where
    stackSize _ = 0

push :: Stack b => a -> b -> a :* b
push = (:*)

pop :: Stack b => a :* b -> (a,b)
pop (x :* y) = (x,y)

dup :: Stack b => a :* b -> a :* a :* b
dup (x :* y) = x :* x :* y

liftBiOp :: Stack rest => (a -> b -> c) -> a :* b :* rest -> c :* rest
liftBiOp f (x :* y :* rest) = push (f x y) rest

add :: (Stack rest, Num a) => a :* a :* rest -> a :* rest
add = liftBiOp (+)

{-
demo: 

*Stacks> stackSize  $ dup (1 :* NilStack)
2

*Stacks> add $ dup (1 :* NilStack)
2 :* NilStack

-}

Поскольку ваш стек варьируется в типе, вы не можете упаковать его в обычную государственную монаду (хотя вы можете упаковать его в параметризованную монаду, но это другая история), но кроме этого, это должно быть просто, приятно и статически проверить Анкет

Answer 2

Это может быть интересно для вас:

https://github.com/gergoerdi/arrow-stack-compiler/blob/master/stackcompiler.hs

Это простой ассемблер, который поддерживает размер стека в своем типе. Например, в следующих двух подписях утверждается, что binOp, Учитывая код, который работает на двух регистрах и оставляет размер стека, создает код, который выводит два аргумента из стека и выдвигает результат. compileExpr Использование binOp и другие конструкции для создания кода, который оценивает выражение и толкает его поверх стека.

binOp :: (Register -> Register -> Machine n n) -> Machine (S (S n)) (S n)
compileExpr :: Expr -> Machine n (S n)

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

Answer 3

Просто и удобно? Я не уверен.

Я бы начал с описания проблемы. Задача состоит в том, чтобы перейти от неформальной в спецификацию, которая ближе к тому, что у нас есть в Haskell (типы).

Здесь есть две проблемы: применение инвариантов на основе типов на языке ввода (арифметические выражения?) И убедиться, что выражение источника, составленное в программу машины стека, на самом деле делает то, что мы хотим.

Первый можно легко решить с помощью GADTS: вам просто нужно индексировать выражения по их типам (например, экспресс A для выражений, которые оценивают значение типа A).

Второй, не так уверен. Конечно, вы можете списки индексов по натуральным натуральным типам (например, с использованием GADTS). Типы определенных функций в списках (таких как голова и хвост), затем становятся достаточно точными, чтобы мы могли сделать их полным. Является ли стопка вашей машины стека однородной (то есть содержит только целые числа или только удваивается или ...)?

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

Answer 4

Я думаю, что это должно быть возможно без проблем, но вы сталкиваетесь с проблемами всякий раз, когда пытаетесь сделать что-то в цикле.Чем вам нужны такие забавные вещи, как натуральные числа на уровне типа.Рассмотрим функцию, подобную этой:

popN :: Int -> Stack (?????)

Но если вам такие вещи не нужны, не стесняйтесь делать все, что захотите.Кстати, циклы работают только в том случае, если количество элементов одинаково до и после, в противном случае они не будут компилироваться.(А-ля бесконечный тип).

Вы могли бы попытаться исправить это с помощью классов типов, но я думаю, для того, что вы пытаетесь сделать, лучше использовать язык с зависимыми типами.