Подъем экзистенциалов до уровня типа - PullRequest
Новая
       70

Подъем экзистенциалов до уровня типа

0 голосов
/ 11 октября 2018

tl; dr: я пытаюсь переписать некоторый код с зависимой типизацией, содержащий список сигма-типов в Haskell, и я не могу сгенерировать синглтоны для экзистенциала, другими словами, этот код завершается ошибкой: 

data Foo :: Type where
  Foo :: forall foo. Sing foo -> Foo

$(genSingletons [''Foo])

Далее следует более длинная версия.

Примите этот код Idris в качестве модели: 

data AddrType = Post | Email | Office

data AddrFields : AddrType -> Type where
  PostFields : (city : String) -> (street : String) -> AddrFields Post
  EmailFields : (email : String) -> AddrFields Email
  OfficeFields : (floor : Int) -> (desk : Nat) -> AddrFields Office

Addr : Type
Addr = (t : AddrType ** AddrFields t)

someCoolPredicate : List AddrType -> Bool

data AddrList : List Addr -> Type where
  MkAddrList : (lst : List Addr) -> {auto prf : So (someCoolPredicate lst)} -> AddrList lst

В основном, когда нам присваивается значение типа AddrList lst, мы знаем, что lst : List Addr, и что someCoolPredicate справедливо для этого списка.

Самое близкое, чего мне удалось достичь в современном Хаскеле, это предположить синглеты-2.5: 

import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List

data AddrType = Post | Email | Office
              deriving (Eq, Ord, Show)

$(genSingletons [''AddrType])
$(singEqInstances [''AddrType])

data family AddrFields (a :: AddrType)

data instance AddrFields 'Post    = PostFields { city :: String, street :: String } deriving (Eq, Ord, Show)
data instance AddrFields 'Email   = EmailFields { email :: String } deriving (Eq, Ord, Show)
data instance AddrFields 'Office  = OfficeFields { flr :: Int, desk :: Int} deriving (Eq, Ord, Show)

data Addr :: Type where
  Addr :: { addrType :: Sing addrType
          , addrTypeVal :: AddrType
          , fields :: AddrFields addrType
          } -> Addr

$(promote [d|
  someCoolPredicate :: [Addr] -> Bool
  someCoolPredicate = ...
  |])

data AddrList :: [Addr] -> Type where
  AddrList :: { addrs :: Sing addrs, prf :: SomeCoolPredicate addrs :~: 'True } -> AddrList addrs

Но как мне на самом деле построить значение этого типа с учетом [Addr]?Другими словами, как я могу выразить что-то вроде следующего в Idris? 

*Addrs> MkAddrList [(Post ** PostFields "Foo" "Bar")]
MkAddrList [(Post ** PostFields "Foo" "Bar")] : AddrList [(Post ** PostFields "Foo" "Bar")]

Проблема в том, что я должен быть в состоянии сделать toSing или эквивалент в списке Addr,но $(genSingletons [''Addr]) не удается.Действительно, даже код в разделе tl; dr не работает.Так что же мне делать, кроме как отказаться от этой идеи?

...