Teknik untuk Melacak Batasan

322

Berikut skenario: Saya sudah menulis beberapa kode dengan tipe tanda tangan dan GHC mengeluh tidak dapat menyimpulkan x ~ y untuk beberapa xdan y. Anda biasanya dapat melempar GHC ke tulang dan menambahkan isomorfisme ke batasan fungsi, tetapi ini adalah ide yang buruk karena beberapa alasan:

  1. Itu tidak menekankan pemahaman kode.
  2. Anda dapat berakhir dengan 5 kendala di mana seseorang akan mencukupi (misalnya, jika 5 tersirat oleh satu kendala lebih spesifik)
  3. Anda dapat berakhir dengan batasan palsu jika Anda melakukan kesalahan atau jika GHC tidak membantu

Saya hanya menghabiskan beberapa jam berjuang melawan 3. Saya bermain dengan syntactic-2.0, dan saya mencoba untuk mendefinisikan versi domain-independen share, mirip dengan versi yang didefinisikan dalam NanoFeldspar.hs.

Saya punya ini:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

dan GHC could not deduce (Internal a) ~ (Internal b), yang jelas bukan tujuan saya. Jadi entah saya telah menulis beberapa kode saya tidak bermaksud (yang memerlukan kendala), atau GHC ingin kendala itu karena beberapa kendala lain yang saya tulis.

Ternyata saya perlu menambahkan (Syntactic a, Syntactic b, Syntactic (a->b))ke daftar kendala, tidak ada yang menyiratkan (Internal a) ~ (Internal b). Saya pada dasarnya menemukan kendala yang benar; Saya masih belum memiliki cara sistematis untuk menemukannya.

Pertanyaan saya adalah:

  1. Mengapa GHC mengusulkan batasan itu? Tidak ada tempat dalam sintaksis yang memiliki kendala Internal a ~ Internal b, jadi dari mana GHC menariknya?
  2. Secara umum, teknik apa yang dapat digunakan untuk melacak asal-usul kendala yang menurut GHC dibutuhkan? Bahkan untuk kendala yang dapat saya temukan sendiri, pendekatan saya pada dasarnya kasar memaksa jalur menyinggung dengan secara fisik menuliskan kendala rekursif. Pendekatan ini pada dasarnya menuruni lubang kelinci tanpa batas dan merupakan metode paling efisien yang dapat saya bayangkan.
haskell constraints ghc crockeea
sumber
21
Sudah ada beberapa diskusi tentang jenis debugger tingkat, tetapi konsensus umum tampaknya menunjukkan logika internal pengetik tidak akan membantu: / Sampai sekarang pemecah kendala Haskell adalah bahasa logika buram jelek :)
Daniel Gratzer
12
@ jozefg Apakah Anda memiliki tautan untuk diskusi itu?
crockeea
36
Seringkali membantu menghapus saja tipe tanda tangan dan membiarkan ghci memberi tahu Anda apa yang seharusnya menjadi tanda tangan.
Tobias Brandt
12
Entah bagaimana adan bterikat - lihat tipe tanda tangan di luar konteks Anda - a -> (a -> b) -> a, tidak a -> (a -> b) -> b. Mungkin itu saja? Dengan pemecah kendala, mereka dapat mempengaruhi kesetaraan transitif di mana saja , tetapi kesalahan biasanya menunjukkan lokasi "dekat" ke tempat kendala itu diinduksi. Itu akan keren meskipun @jozefg - mungkin memberi batasan pada tag atau sesuatu, untuk menunjukkan dari mana asalnya? : s
Athan Clark

Jawaban:

6

Pertama-tama, fungsi Anda memiliki tipe yang salah; Saya cukup yakin itu harus (tanpa konteks) a -> (a -> b) -> b. GHC 7.10 agak lebih membantu dalam menunjukkan hal itu, karena dengan kode asli Anda, ia mengeluh tentang kendala yang hilang Internal (a -> b) ~ (Internal a -> Internal a). Setelah memperbaiki sharetipe, GHC 7.10 tetap membantu dalam memandu kami:

  1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

  2. Setelah menambahkan di atas, kita dapatkan Could not deduce (sup ~ Domain (a -> b))

  3. Setelah menambahkan itu, kita dapatkan Could not deduce (Syntactic a), Could not deduce (Syntactic b)danCould not deduce (Syntactic (a -> b))

  4. Setelah menambahkan ketiga ini, akhirnya ketikkan centang; jadi kita berakhir dengan

    share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          Domain (a -> b) ~ sup,
          Internal (a -> b) ~ (Internal a -> Internal b),
          Syntactic a, Syntactic b, Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) fi)
      => a -> (a -> b) -> b
share = sugarSym Let

Jadi saya katakan GHC tidak berguna dalam memimpin kita.

Adapun pertanyaan Anda tentang melacak dari mana GHC mendapatkan persyaratan kendala dari, Anda dapat mencoba bendera debugging GHC , khususnya -ddump-tc-trace,, dan kemudian membaca log yang dihasilkan untuk melihat di mana Internal (a -> b) ~ tdan (Internal a -> Internal a) ~ tditambahkan ke Wantedset, tetapi itu akan cukup lama dibaca .

Kaktus
sumber
0

Apakah Anda mencoba ini di GHC 8.8+?

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi,
          _) 
      => a -> (a -> b) -> a
share = sugarSym Let

Kuncinya adalah menggunakan tipe lubang di antara kendala: _ => your difficult type

Michal Gajda
sumber