5

Haskell に制約を強制するメカニズムはありますunsafeCoerceか?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module CatAdjonctionsSOQuestion where

import Data.Proxy
import Data.Tagged
import Unsafe.Coerce

newtype K a ph = K {unK :: a} -- I would want c a => c ((K a) i) for any c :: Constraints

-- I could do any possible instance by hand
deriving via a instance Semigroup a => Semigroup ((K a) i)

-- I want them all
-- deriving via a instance c ((K a) i) -- Instance head is not headed by a class: c (K a i)

data Exists c where
  Exists :: c a => a -> Exists c

data ExistsKai c i where
  ExistsKai :: c ((K a) i) => Proxy a -> ExistsKai c i

ok :: forall x c i. (forall x. (forall a. c a => a -> x) -> x) -> (forall a. c ((K a) i) => Tagged a x) -> x
ok s k =
  let e = (s Exists :: Exists c)
   in let f = unsafeCoerce e :: ExistsKai c i
       in case f of (ExistsKai (Proxy :: Proxy a)) -> unTagged (k @a)
4

1 に答える 1

3

親切にチェックできるように少し修正して、お願いします

newtype K a ph = K {unK :: a}
-- I would want c a => c ((K a) i)
-- for any c :: Type -> Constraint

それは無効であるため、今もこれからも絶対に入手できません。検討

(~) Bool :: Type -> Constraint

今(~) Bool Boolは成り立ちますが、絶対に を達成することはできません(~) Bool (K Bool i)。

平等制約なしではどうですか？まあ、ライプニッツの等式を使ってそれもできます:

class Bar a where
  isBool :: f a -> f Bool

instance Bar Bool where
  isBool = id

しかし、誰が底を打たないかを書く方法はinstance Bar (K Bool i)ありisBoolません。

于 2021-05-16T16:45:38.597 に答える