Линейные и уникальные типы с mkPair
Я читал эту статью здесь http://edsko.net/2017/01/08/linearity-in-haskell/ и автор упоминает, что можно создать неуникальный массив с уникальными элементами, но вы можете ' не извлекай их.
Т.е.
mkPair :: 1:a -> 1:b -> ω:(1:a, 1:b) -- correct but useless
mkPair x y = (x, y)
но не могли бы вы прочитать элементы один раз в вызывающей функции? Может быть, я что-то упустил.
Кроме того, хотя эта функция и легальна, она недопустима, если рассматривать ее с точки зрения линейности. Но я думал, что это всего лишь две стороны одной медали, поэтому функция не изменит легальность в зависимости от перспективы.
2 ответа
Я не уверен, что автор сообщения в блоге имеет в виду, когда говорит, что это правильно, но бесполезно. В Clean, языке, который фактически реализовал типы уникальности, это не разрешено из-за распространения уникальности. Вы можете прочитать больше об этом в разделе 9.2 языкового отчета. Там просто не существует тип ω:(1:a, 1:b) (который (*a,*b) в чистом синтаксисе), потому что из-за распространения уникальности это на самом деле 1:(1:a, 1:b) или же *(*a,*b),
Это может быть то, что автор пытается выразить, но я считаю, что сообщение трудно прочитать из-за отсутствия теоретической основы.
На самом деле, mkPair неправильно напечатан (как утверждает сам блог), так как его тип возврата позволяет дублировать полученную пару. Итак, любой вызывающий объект, имеющий уникальные значения типов a а также b, может составить пару, продублировать ее, взять четыре компонента (по два от каждой пары) и получить два значения типа aи два значения типа b,
Это позволит обойти линейность a а также b, поэтому не должно быть функции, имеющей тип mkPair Вы показываете выше.