Mengapa daftar tipe ghci desugar dan tipe famili? Bisakah ini dinonaktifkan secara selektif?

93

Saya mencoba membuat jenis tampilan ghci untuk perpustakaan saya seintuitif mungkin, tetapi saya mengalami banyak kesulitan saat menggunakan fitur jenis yang lebih canggih.

Katakanlah saya memiliki kode ini dalam sebuah file:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data Container (xs::[*]) = Container

Saya memuatnya di ghci, lalu saya mengetik perintah berikut:

ghci> :t undefined :: Container '[String,String,String,String,String]

Sayangnya, ghci memberi saya tampilan yang agak jelek:

:: Container
       ((':)
          *
          String
          ((':)
             * String ((':) * String ((':) * String ((':) * String ('[] *))))))

ghci telah menghilangkan gula untuk string level tipe. Apakah ada cara untuk mencegah ghci melakukan ini dan memberi saya versi yang cantik?

Pada catatan terkait, katakanlah saya membuat Replicatefungsi level tipe

data Nat1 = Zero | Succ Nat1

type family Replicate (n::Nat1) x :: [*]
type instance Replicate Zero x = '[]
type instance Replicate (Succ n) x = x ': (Replicate n x)

type LotsOfStrings = Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String

Sekarang, ketika saya meminta ghci untuk suatu tipe menggunakan LotsOfStrings:

ghci> :t undefined :: Container LotsOfStrings

ghci bagus dan memberi saya hasil yang bagus:

undefined :: Container LotsOfStrings

Tetapi jika saya meminta Replicateversi d,

ghci> :t undefined :: Container (Replicate (Succ (Succ (Succ (Succ (Succ Zero))))) String)

ghci menggantikan tipe family ketika tidak melakukannya untuk sinonim tipe:

:: Container
       ((':)
          *
          [Char]
          ((':)
             * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

Mengapa ghci melakukan substitusi untuk keluarga tipe, tetapi bukan sinonim tipe? Apakah ada cara untuk mengontrol kapan ghci akan melakukan substitusi?

haskell types ghci Mike Izbicki
sumber
7
Karena tipe sinonim dirancang murni untuk konsumsi manusia - itu tidak membuat substitusi karena mengakui bahwa Anda membuat sinonim tipe karena Anda ingin menulis / melihat tipe seperti itu. Itu membuat substitusi dengan tipe keluarga karena keluarga tipe benar-benar tentang menghitung / menyimpulkan tipe, bukan menampilkannya.
AndrewC
Solusi untuk masalah Anda ada dalam pertanyaan Anda - buat sinonim tipe jika Anda ingin menyingkat.
AndrewC
2
@AndrewC Saya baru saja memikirkan pertanyaan lain terkait dengan komentar Anda: Mengapa jenis String terkadang ditampilkan sebagai [Char]dan terkadang ditampilkan sebagai String?
Mike Izbicki
1
Saya pikir ghci mencoba untuk mempertahankan jenis sinonim yang ditemukannya di sumbernya. Artinya, jika suatu fungsi dideklarasikan sebagai tipe String->String, maka tipe hasilnya akan ditampilkan sebagai String. Namun jika itu harus membangun tipe dari potongan, seperti misalnya "abc"(yang sama dengan 'a':'b':'c':[]) tidak ada sinonim untuk dipertahankan. Ini murni spekulasi.
n. 'kata ganti' m.
4
@nm: Perhatikan bahwa GHC melakukan upaya serupa untuk mempertahankan nama variabel jenis, saat jenis simpulan yang lebih umum bersatu dengan variabel jenis yang kurang umum dan dinamai secara eksplisit. Saya menduga bahwa jika tipe eksplisit Stringdisatukan dengan variabel tipe f aatau [a], itu akan ditampilkan [Char]setelahnya karena alasan yang sama.
CA McCann

Jawaban:

2

Solusi yang saya tahu adalah menggunakan: jenis. Misalnya,

ghci>: kind (Container '[String, String, String, String, String])

Memberikan:

(Penampung '[String, String, String, String, String]) :: *

Sementara

ghci>: baik! (Penampung '[String, String, String, String, String])

Akan mencetak sesuatu seperti ini:

Wadah

((':)

  *
  [Char]
  ((':)
     * [Char] ((':) * [Char] ((':) * [Char] ((':) * [Char] ('[] *))))))

Secara resmi, tentu saja, Anda menanyakan pertanyaan lain kepada ghci kind, tetapi berhasil. undefined ::Bagaimanapun menggunakan adalah semacam solusi, jadi saya pikir ini mungkin cukup.

pengguna2141650
sumber
Saya hanya menggunakan undefined ::untuk memberikan contoh yang mudah. Masalah sebenarnya adalah ketika Anda mendapatkan pesan kesalahan yang memiliki jenis daftar seribu jenis yang berbeda. Dibutuhkan halaman untuk mencetaknya, dan sangat sulit untuk diurai.
Mike Izbicki
Ya, cukup adil. Coulda menyadari itu. Saya berutang jawaban yang lebih baik
user2141650
2

Ini diperbaiki dalam GHC 7.8 mendatang.

GHC 7.6 mencetak jenis jika tipe data menggunakan PolyKinds. Jadi Anda melihat, (':) * String ('[] *)bukan hanya (':) String '[].

Di GHC 7.8, jenis tidak lagi ditampilkan secara default dan jenis data Anda cukup dicetak sebagai daftar, seperti yang Anda harapkan. Anda dapat menggunakan bendera baru -fprint-explicit-kindsuntuk melihat jenis eksplisit seperti di GHC 7.6. Saya tidak tahu alasannya, mungkin jenis eksplisit dimaksudkan untuk membantu memahami PolyKinds.

sdcvvc.dll
sumber
0 
import GHC.TypeLits

data Container (xs::[*]) = Container

Saya memuatnya di ghci, lalu saya mengetik perintah berikut:

:t undefined :: Container '[String,String,String,String,String]
ئیترده ڕۆم
sumber
Begitu...? Anda masih mendapatkan hasilnya kembali menurut saya kira, yaitu String ((':) * String ((':) * String ((':) * ....
kiri sekitar sekitar