Проверка на уровне уровня

Question

Скажем, я хотел бы построить подтипы, удовлетворяющие определенным инвариантам, без помощи внешних инструментов, таких как LiquidHaskell (в идеале я хочу сделать это даже без типов). Какой самый элегантный способ сделать это? До сих пор я попытался следующие:

class Validated a where 
    type Underlying a 
    validate :: Underlying a -> Bool 
    construct :: Underlying a -> a 
    use :: a -> Underlying a 

makeValidated :: Validated a => Underlying a -> Maybe a 
makeValidated u = if validate u 
        then Just (construct u) 
        else Nothing 


newtype Name = Name String 
instance Validated Name where 
    type Underlying Name = String 
    validate str = and [ isUppercase (str !! 0) 
         , all isLetter str ] 
    construct = Name 
    use (Name str) = str 

Я полагаю, что если я не экспортировать «Name» конструктор из модуля, у меня будет рабочее решение, потому что единственный способ построить элемент типа будет через makeValidated function.

Однако компилятор жалуется, как например:

Could not deduce (Underlying a0 ~ Underlying a) 
from the context (Validated a) 
    bound by the type signature for 
      makeValidated :: Validated a => Underlying a -> Maybe a 
    at validated.hs:11:18-55 
NB: `Underlying' is a type function, and may not be injective 
The type variable `a0' is ambiguous 
Possible fix: add a type signature that fixes these type variable(s) 
In the first argument of `validate', namely `u' 
In the expression: validate u 
In the expression: 
    if validate u then Just (construct u) else Nothing 

Как я могу это исправить?

Answer 1

Underlying - это функция типа, которая не может быть инъективной. То есть:

instance Validate T1 where 
    type Underlying T1 = Int 
    validate = ... -- code A 

instance Validate T2 where 
    type Underlying T2 = Int 
    validate = ... -- code B 

Рассмотрим теперь

validate (42 :: Int) 

Что это должен делать? Должен ли он вызывать код A или B? С Underlying T1 = Underlying T2 = Int невозможно сказать.

Невозможно называть validate однозначно. Чтобы избежать этого, можно исправить это добавить параметр «прокси» для вашей функции проверки:

data Proxy a = Proxy 

class Validate a where 
    validate :: Proxy a -> Underlying a -> Bool 

Теперь вы можете использовать:

validate Proxy (42 :: Int)    -- still ambiguous! 
validate (Proxy :: Proxy T1) (42 :: Int) -- Now OK! 
validate (Proxy :: Proxy T2) (42 :: Int) -- Now OK! 

Answer 2

Функция validate, как написано, не используется в текущем GHC. Глядя на его тип подписи:

validate :: Validated a => Underlying a -> Bool 

вы могли бы разумно думать, что, учитывая значение типа Underlying a, можно выяснить, какие Validated экземпляр для использования, а именно a один. Но это ошибка: поскольку Underlying не является инъективным, могут быть типы b и c, для которых Underlying b ~ Underlying c; следовательно, ни b, ни c не могут быть каноническим выбором, для какого экземпляра использовать. То есть is нет хорошего отображения F по типам, для которых F (Underlying a) ~ a всегда верен!

Альтернативой может быть использование семейства данных, а не семейства типов.

class Validated a where 
    data Underlying a 
    validate :: Underlying a -> Bool 

instance Validated Name where 
    data Underlying Name = Underlying String 
    validate (Underlying name) = ...