История изменений
Исправление hateyoufeel, (текущая версия) :
Таким образом вопрос о том является ли Void а функтором сводится к вопросу готовы ли мы считать реализацию через error как отображение.
Использование error строго не обязательно. Например:
ghci> data Void1 a
ghci> :info Void1
type role Void1 phantom
type Void1 :: forall {k}. k -> *
data Void1 a
-- Defined at <interactive>:1:1
ghci> instance Functor Void1 where fmap f v = fmap f v
ghci> :t fmap @Void1
fmap @Void1 :: Functor Void1 => (a -> b) -> Void1 a -> Void1 b
Так как множества значений Void1 a является пустым (плюс bottom) для любого a, то fmap f даёт нам функцию Void1 a -> Void1 b, т.е. из пустого множества в пустое множество. Та самая тривиальная стрелка.
ghci> let f = show; f :: Int -> String
ghci> :t fmap @Void1 f
fmap @Void1 f :: Void1 Int -> Void1 String
По тем же собственно причинам, мы не сможем построить функцию Void a -> Void b
Но вот я построил её выше. Она принимает единственное возможное значение из типа Void1 Int и возвращает единственное возможное значение из типа Void1 String, то есть bottom.
Исправление hateyoufeel, :
Таким образом вопрос о том является ли Void а функтором сводится к вопросу готовы ли мы считать реализацию через error как отображение.
Использование error строго не обязательно. Например:
ghci> data Void1 a
ghci> :info Void1
type role Void1 phantom
type Void1 :: forall {k}. k -> *
data Void1 a
-- Defined at <interactive>:1:1
ghci> instance Functor Void1 where fmap f v = fmap f v
ghci> :t fmap @Void1
fmap @Void1 :: Functor Void1 => (a -> b) -> Void1 a -> Void1 b
Так как множества значений Void1 a является пустым (плюс bottom) для любого a, то fmap f даёт нам функцию Void1 a -> Void1 b, т.е. из пустого множества в пустое множество. Та самая тривиальная стрелка.
ghci> let f = show; f :: Int -> String
ghci> :t fmap @Void1 f
fmap @Void1 f :: Void1 Int -> Void1 String
По тем же собственно причинам, мы не сможем построить функцию Void a -> Void b
Но вот я построил её выше. Она принимает единственное возможное значение из типа Void Int и возвращает единственное возможное значение из типа Void String, то есть bottom.
Исходная версия hateyoufeel, :
Таким образом вопрос о том является ли Void а функтором сводится к вопросу готовы ли мы считать реализацию через error как отображение.
Использование error строго не обязательно. Например:
ghci> data Void1 a
ghci> :info Void1
type role Void1 phantom
type Void1 :: forall {k}. k -> *
data Void1 a
-- Defined at <interactive>:1:1
ghci> instance Functor Void1 where fmap f v = fmap f v
ghci> :t fmap @Void1
fmap @Void1 :: Functor Void1 => (a -> b) -> Void1 a -> Void1 b
Так как множества значений Void1 a является пустым (плюс bottom) для любого a, то fmap f даёт нам функцию Void1 a -> Void1 b, т.е. из пустого множества в пустое множество. Та самая тривиальная стрелка.
ghci> let f = show; f :: Int -> String
ghci> :t fmap @Void1 f
fmap @Void1 f :: Void1 Int -> Void1 String
По тем же собственно причинам, мы не сможем построить функцию Void a -> Void b
Но вот я построил её выше.