Кстати ещё typelevel вопрос. Представим что у меня есть data

Question

Кстати ещё typelevel вопрос. Представим что у меня есть data

X = A | B и data Gadt (p :: X) where GA :: Gadt A, GB :: Gadt B, а я хочу штуку вида f :: SomeConstraint p => Gadt p, чтобы f @A,f @B бы работали, это можно без unsafe coerce делать нормально? Понятно, что можно таскать там что то вроде Either (Refl a A) (Refl a B), но такое неудобно использовать для более больших X

#haskell #programming #russian

0

03.02.2022

8 ответов

35 просмотров

Anton Sorokin Автор вопроса

TOV_MULTIMASSO
Да и так должно вроде работать

как?

0

03.02.2022

Anton Sorokin Автор вопроса

TOV_MULTIMASSO
Да и так должно вроде работать

f @A =... нельзя же писать, и например class KnownX (p :: X) where knownX :: X не поможет компилятору по терму понять что у нас он их нужного типа пришёл (только с unsafeCoerce ему помочь можно)

0

03.02.2022

кана

не очень понял где ты тут хочешь unsafeCoerce, но делается это просто {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeApplications #-} data X = A | B data Gadt (p :: X) where GA :: Gadt A; GB :: Gadt B class MkGadt p where mkGadt :: Gadt p instance MkGadt A where mkGadt = GA instance MkGadt B where mkGadt = GB f :: MkGadt p => Gadt p f = mkGadt x = f @A y = f @B

0

03.02.2022

Anton Sorokin Автор вопроса

кана
не очень понял где ты тут хочешь unsafeCoerce, но ...

Я хочу чтобы mkGadt было одной функцией

0

03.02.2022

TOV_MULTIMASSO

Anton Sorokin
f @A =... нельзя же писать, и например class Known...

import Data.Proxy?

0

03.02.2022