• ? code Haskell typefun
    есть у меня метод:
    
    
    hexp :: S s a -> H s a
    
    но он не совсем верен, на самом деле он должен выглядеть как:
    
    hexp :: S s a -> H s a -- для тех `a` которые не будут выведены в конретный тип по S s a
    hexp :: S s a -> H s b -- во всех остальных случаях.
    
    Реально ли?

Replies (13)

  • @qnikst, Как понять "не будут выведены в конкрентый тип по S s a"
  • @fmap, т.е. если type infer будет происходить не по H s a
    в смысле пусть есть foo :: H s Int, тогда если есть код
    foo (hexp s) — то s выведется как `S s Int` чего я не хочу.

    Но я хочу обратного если известно, что s :: S s Int, то hexp s точно будет foo s :: H s Int
  • @qnikst, Если только для определенных типов: hexp :: S s a -> H s (F a b); type family F a b :: *; type instance F A b = A; type instance F B b = B; ...; type instance F a b = b;
  • @fmap, ну вот я тоже подумал, что через тайпфемили и неиньективность можно (хотя тут кайнд MyType -> *, так что может и нету неиньективности)
  • @fmap, ещё можно фендепы попробовать :

    class Foo a b | a -> b where .. тогда а не будет выводиться если известно b и наоборот b выводится, если известно a
  • @qnikst, В HM такого точно нельзя сделать.
  • @fmap, {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE FunctionalDependencies #-}
    module Main where

    class Foo a b | a -> b where
    fooCoerce :: a -> b

    instance Foo Int Int where fooCoerce = id
    instance Foo Double Double where fooCoerce = id


    newtype S a = S { unS :: a}
    newtype H a = H { unH :: a}

    foo :: Foo a b => S a -> H b
    foo (S x) = H (fooCoerce x)

    test1 = foo (S (3::Int))

    test2 = case foo (S (3::Int)) of
    H x -> (x + (1::Int))

    — не компилируется
    — test3 = case foo (S 3) of
    — H x -> (x + (1::Int))
  • @qnikst, а вот с instance Foo a a where fooCoerce = id — компилируется
  • @qnikst, Тут та же проблема как в /4? А какой use case у /0?
  • @fmap, есть данные приходящие из FFI кода: S s a (грубо говоря враппер вокруг pointer), есть GADT (H s a) их описывающий с конструкторами для каждого конкретного a. Есть метод hexp :: S s a -> H s a, который работает примерно так:
    unsafeInlinIO . . peek . unS, где peek это

    peek :: Ptr (H s a) -> H s a
    peek p = case typeOf p of
    C1 -> unsafeCoerce $ realPeek (unsafeCoerce p)
    ....

    в итоге эта байда сносит ghc крышу. Проблема тут в том, что а). мне кажется что в оптимизациях есть баг судя по генерируемым стейджам), б). 'a' не всегда выводится верно.

    Для S есть экзестенциальный тип SomeS, который выдается когда настоящий S неизвестен, и там это спасает. Но тут как-то все хуже, у меня есть:

    case (hexp . (cast :: SSINGTYPE a -> SomeSEXP s -> S s a) R.Int s) of
    тут case повсем возможным веткам

    так вот я думаю, как мы уменьшить ghc ум, чтобы он лишнего не выводил и ленюсь дебажить..
  • @qnikst, вот `case typeOf` с парой unsafeCoerce тут намекает на то, что нахрен все переписать надо...
  • @qnikst, а ещё про струкруру GADT, почти для всех типов это H s (ConcreteType), но есть пара конструктуров которые имеют тип `H s a`, это скорее всего важно здесь