AK
Я, вроде, также, но вот предел, похоже я неправильно понял
Size: a a a
2020 February 23
AK
поэтому если вы напишете Double - это будет определением какого-то дельта
Какую информацию должен сохранить константный функтор?
Oℕ
ну если хотите хаскель пожалуйста
функтор из дискретной категории не требует задания стрелок
функтор из дискретной категории не требует задания стрелок
Oℕ
поэтому функтор из дискретной из двух объектов в Hask выражается как семейство типов кайнда
Bool -> TypeAK
Что тогда является объектами в индексной категории?
Oℕ
константный функтор - это семейство вроде
type family ConstDouble
ConstDouble True = Double
ConstDouble False = Double
type family ConstDouble
ConstDouble True = Double
ConstDouble False = Double
Oℕ
Что тогда является объектами в индексной категории?
в произвольной индексной категории - что-угодно, т.к. любая категория может выступать как индексная
Oℕ
соответственно, для задания конуса вам нужно ест. преобразование
forall (b :: Bool). ConstDouble t -> f t
forall (b :: Bool). ConstDouble t -> f t
Oℕ
соответственно, если вы задали диаграммный функтор как
type family StringAndInt
StringAndInt True = String
StringAndInt False = Int
type family StringAndInt
StringAndInt True = String
StringAndInt False = Int
AK
константный функтор - это семейство вроде
type family ConstDouble
ConstDouble True = Double
ConstDouble False = Double
type family ConstDouble
ConstDouble True = Double
ConstDouble False = Double
Я не знал, что на хаскеле можно значения использовать в семействах, думал, что только типы
Oℕ
то ваше ест. преобразование должно выглядеть как
forall (b :: Bool) . ConstDouble b -> StringAndInt b
forall (b :: Bool) . ConstDouble b -> StringAndInt b
Oℕ
Я не знал, что на хаскеле можно значения использовать в семействах, думал, что только типы
LANGUAGE DataKinds
Oℕ
то ваше ест. преобразование должно выглядеть как
forall (b :: Bool) . ConstDouble b -> StringAndInt b
forall (b :: Bool) . ConstDouble b -> StringAndInt b
что превращается в пару функций Double -> Int, Double -> String
AK
Во, вот это я и не понял. Почему в индексной категории не два типа, а два значения?
AK
Но с датакайнд это получаются два типа
AK
Что-то вроде двух разных юнитов
AK
Или опять мимо?
AK
Мне надо помедитировать. Спасибо!
Oℕ
Не все категории состоят из типов
Oℕ
объект != тип