Неявное приведение к типу * stati c (принуждение) в Haskell - PullRequest
Новая
       69

Неявное приведение к типу * stati c (принуждение) в Haskell

9 голосов
/ 09 марта 2020

Проблема

Рассмотрим следующую проблему проектирования в Haskell. У меня есть простой символьный c EDSL, в котором я хочу express переменных и общих выражений (многомерных полиномов), таких как x^2 * y + 2*z + 1. Кроме того, я хочу express определенных символов c уравнений над выражениями, скажем x^2 + 1 = 1, а также определений , например, x := 2*y - 2.

Цель состоит в том, чтобы:

  1. Имеет отдельный тип для переменных и общих выражений - некоторые функции могут применяться к переменным, а не к сложным выражениям. Например, оператор Definition := может иметь тип (:=) :: Variable -> Expression -> Definition, и не должно быть возможности передать сложное выражение в качестве его левого параметра (хотя должно ). можно передать переменную в качестве ее правого параметра без явного приведения ).
  2. иметь выражения с экземпляром Num, чтобы можно было добавлять целые литералы в выражения и использовать удобную запись для общих алгебраических c операций, таких как сложение или умножение, без введения некоторых вспомогательных операторов-оберток.

Другими словами, я хотел бы иметь неявное и stati c приведение типа (приведение) переменных к выражениям. Теперь я знаю, что в Haskell нет неявных приведений типов. Тем не менее, определенные концепции объектно-ориентированного программирования (в данном случае простое наследование) являются выразимыми в системе типов Haskell, с расширениями языка или без них. Как я могу удовлетворить оба вышеупомянутых пункта, сохраняя легкий синтаксис? Это вообще возможно?

Обсуждение

Понятно, что основная проблема здесь - ограничение типа Num, например,

(+) :: Num a => a -> a -> a

В принципе, можно написать один (обобщенный) алгебраический тип данных c для переменных и выражений. Тогда можно было бы написать := таким образом, чтобы выражение левой части распознавалось, и принимался только конструктор переменной, в противном случае - ошибка времени выполнения. Это, однако, не чистое, stati c (то есть время компиляции) решение *

Пример

В идеале я хотел бы получить легкий синтаксис, такой как 

computation = do
  x <- variable
  t <- variable

  t |:=| x^2 - 1
  solve (t |==| 0)

В частности, я хочу запретить нотацию, такую ​​как t + 1 |:=| x^2 - 1, поскольку := должно давать определение переменной, а не целое выражение в левой части.

1 Ответ

8 голосов
/ 09 марта 2020

Чтобы использовать полиморфизм, а не подтип (потому что это все, что у вас есть в Haskell), не думайте, что «переменная является выражением», но «переменные и выражения имеют некоторые общие операции». Эти операции могут быть помещены в класс типов: 

class HasVar e where fromVar :: Variable -> e

instance HasVar Variable where fromVar = id
instance HasVar Expression where ...

Затем, вместо того, чтобы приводить вещи, сделать вещи полиморфными c. Если у вас есть v :: forall e. HasVar e => e, его можно использовать как в качестве выражения, так и в качестве переменной. 

example :: (forall e. HasVar e => e) -> Definition
example v = (v := v)  -- v can be used as both Variable and Expression

 where

  (:=) :: Variable -> Expression -> Definition

Skeleton для создания кода ниже проверки типов: https://gist.github.com/Lysxia/da30abac357deb7981412f1faf0d2103

computation :: Solver ()
computation = do
  V x <- variable
  V t <- variable
  t |:=| x^2 - 1
  solve (t |==| 0)
...