• code Haskell
    import Data.Proxy
    import Data.Kind
    
    type family Saturate (f :: k) (v :: a) :: Type where
        Saturate (f :: a -> Type) v = f v
        Saturate (f :: a -> k)    v = Saturate (f v) v
    
    data Select f = Select (forall a. Saturate f a -> a)
    
    sel :: Proxy f -> (forall a. Saturate f a -> a) -> Select f
    sel _ = Select
    
    data T a b c = T { x :: a, y :: b, z :: c }
    
    Есть такой кусочек кода. Всё как всегда:
    Select x — реджектится компилятором (без явной аннотации типа) потому что из Saturate f a нельзя вывести f.
    sel x — работает, но таскать Proxy (или явную аппликацию типа) не хочется.
    Есть шанс сделать красиво?

Replies (3)