• ? Haskell typefun а чего у меня rewrite rule не заводятся?

    newtype Tagged n s = Tagged n

    sort2 :: Ord a => Tagged [a] s -> Tagged [a] Sorted
    sort2 = Tagged . trace "sorting.." . List.sort . coerce
    {-# NOINLINE[1] sort2 #-}

    {-# RULES
    "sort/Sorted" forall (x :: Tagged a Sorted). sort2 x = x
    #-}

    main = print $ sort2 . sort2 $ voidT [1..3]

Replies (2)

  • @qnikst, на классотипах вот будет работать:

    class Sort1 s where
    sort1 :: Ord a => Tagged [a] s -> Tagged [a] Sorted
    sort1 = Tagged . trace "sorting.." . List.sort . coerce

    instance Sort1 Sorted where
    sort1 = id
  • @qnikst, тут естественно в тегах должен быть Type level list, и вместо четкого Sorted проверка констрейнта, но и так уже интересно как можно сделать..

    да, желателен эффект, чтобы вместо второй сортировки был id.