申し込むときに「何の団体か」というのを記述する欄がありまして、そこに記述しておくとOSC公式サイトに団体名やURLが掲載されたりするのでせっかくなら個人枠ではなくHaskell-JP枠で出場した方が宣伝効果もあって良いかなと思いまして。
without :: Membership xs x -> (h :* xs) -> (h :* ys) without k = hfoldrWithIndex (\i e r -> if k == i then r else e <: r) nil
ys と xs の関係をうまく推論できないのか、型エラーになってしまいます。ys ⊆ xs というのをつかえば行けると思います
app\Main.hs:37:3: error:
? Could not deduce: ys ~ '[]
from the context: Include xs ys
bound by the type signature for:
without :: forall (xs :: [*]) (ys :: [*]) x (h :: * -> *).
Include xs ys =>
Membership xs x -> (h :* xs) -> h :* ys
at app\Main.hs:35:1-71
‘ys’ is a rigid type variable bound by
the type signature for:
without :: forall (xs :: [*]) (ys :: [*]) x (h :: * -> *).
Include xs ys =>
Membership xs x -> (h :* xs) -> h :* ys
at app\Main.hs:35:1-71
Expected type: (h :* xs) -> h :* ys
Actual type: (h :* xs) -> h :* '[]
? In the expression:
hfoldrWithIndex (\ l e r -> if k == l then r else e <: r) nil
In an equation for ‘without’:
without k
= hfoldrWithIndex (\ l e r -> if k == l then r else e <: r) nil
? Relevant bindings include
without :: Membership xs x -> (h :* xs) -> h :* ys
(bound at app\Main.hs:36:1)
|
37 | hfoldrWithIndex (\l e r -> if k == l then r else e <: r) nil
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
app\Main.hs:37:52: error:
? Couldn't match type ‘'[x1]’ with ‘'[]’
Expected type: h :* '[]
Actual type: h :* '[x1]
? In the expression: e <: r
In the expression: if k == l then r else e <: r
In the first argument of ‘hfoldrWithIndex’, namely
‘(\ l e r -> if k == l then r else e <: r)’
? Relevant bindings include
e :: h x1 (bound at app\Main.hs:37:23)
l :: Membership xs x1 (bound at app\Main.hs:37:21)
|
37 | hfoldrWithIndex (\l e r -> if k == l then r else e <: r) nil
| ^^^^^^
ys が [] だったり要素が入っていたりすることが伝わっていないみたいですね。。。 :thinking_face:without :: (Include xs ys) => Membership xs x -> (h :* xs) -> (h :* ys) without k = hfoldrWithIndex (\l e r -> if k == l then r else e <: r) nil