Корректировка индексированных ограничений в haskell

Question

Возможно ли сделать точечную корреляцию индексированных ограничений в Haskell?

{-# LANGUAGE KindSignatures           #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE MultiParamTypeClasses        #-}
{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE ConstraintKinds        #-}


import Data.Kind


class Paramed t where
   type Cxt0 t :: Constraint
   type Cxt2 t :: (* -> *) -> Constraint

data And a b

instance (Paramed a, Paramed b) => Paramed (And a b) where
   type Cxt0 (And a b) = (Cxt0 a, Cxt0 b) -- OK
   --type Cxt2 (And a b) = (\@m -> ((Cxt2 a m, Cxt2 b m))) -- does not work
   type Cxt2 (And a b) m = (Cxt2 a m, Cxt2 b m) -- does not work either

Это приводит к следующему

error:
    • Number of parameters must match family declaration; expected 1
    • In the type instance declaration for ‘Cxt2’
      In the instance declaration for ‘Paramed (And a b)’

Answer 1

Вам, вероятно, нужно использовать именованный класс, то есть что-то вроде

instance (Paramed a, Paramed b) => Paramed (And a b) where
   type Cxt0 (And a b) = (Cxt0 a, Cxt0 b) -- OK
   type Cxt2 (And a b) = C a b

class (Cxt2 a m, Cxt2 b m) => C a b (m :: * -> *) where
instance (Cxt2 a m, Cxt2 b m) => C a b m where

, включающее неразрешимые экземпляры.(Конечно, вы можете использовать другое имя, отличное от C)

В Haskell, тип * -> * не заселен лямбдами, такими как \ t -> [t], поскольку там нет лямбд на уровне типов.Нам нужно объявить именованный тип (используя data или newtype) и использовать его для заселения * -> *.

Вид * -> Constraint аналогичен: вам нужен именованный класс.То же самое для (* -> *) -> Constraint или любого другого ... -> Constraint вида.

Если я правильно помню, необходимо использовать именованный тип / класс, чтобы сделать вывод типа возможным.