Repline не пробовал?

Нет, выглядит интересно конечно

когда нечего лифтить, то и лифтить не надо

зачем делать столько ридеров вместо одного не ясно

🤔🤔🤔🤔

Привет. Я пытаюсь сделать авторизацию с помощью метода, описанного в Ghost of Departed Proof. У меня есть тип CanDeleteUser, который может создаваться только в специальном модуле, извне создать значения данного типа нельзя. Есть функция deleteUser, принимающая CanDeleteUser в качестве доказательства, что текущий пользователь может удалить другого пользователя. Если передать в качестве первого аргумента undefined, то пользователь удалится. Есть ли какой-нибудь способ заставить функции, использующие данный тип, вычислять его значения до WKNF?

deleteUser :: CanDeleteUser userId deleteId
          -> Named userId (AuthResult (Entity User))
          -> Named deleteId (Key User)
          -> AppM NoContent

да, просто сматчить

Это я понимаю. Но, мне как пользователю данного типа ничто не мешает не матчить

data CanDeleteUser userId deleteId = Can
deleteUser :: CanDeleteUser userId deleteId -> ...
deleteUser Can = ...

или

deleteUser !_ = ...

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

а вот тот кто уже будет пользоваться deleteUser не сможет передать undefined

есть еще один способ сделать это, чтобы undefined было передать намного сложнее - перенести из явнопередавемых аргументов в констрейнты

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Unsafe.Coerce

class CanDelete

delete :: CanDelete => IO ()
delete = print "delete"

newtype X c a = X (c => a)

withAccessToDelete :: forall a. (CanDelete => a) -> a
withAccessToDelete x = unsafeCoerce (X x :: X CanDelete a) ()

main = do
 -- delete -- impossible
 withAccessToDelete do
   delete

Надо будет почитать что-то на эту тему, сейчас выглядит, как магия

но это не особо нужно, там я выше описал как нужно делать

deleteUser это все еще функция из того модуля, где и CanDelete должен быть, она знает про конструктор и знает, что он нужен. А вот вне ее использовать deleteUser с undefined уже не выйдет

Кпна, как ты столько узнал о хаскеле не прочтя ни одной книги?🤔

Чисто доку читал?

из этого чатика

ну способ выше я узнал, прочитав сорцы reflection, там это используется для эмуляции имплиситов

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