tritlo@nietzsche:~/Haskell2018$ ghci
GHCi, version 8.6.1: http://www.haskell.org/ghc/ :? for help
Loaded package environment from /home/tritlo/Haskell2018/.ghc.environment.x86_64-linux-8.6.1
Loaded GHCi configuration from /home/tritlo/Haskell2018/.ghci
λ> ( _ "hello") :: [String]
<interactive>:1:3: error:
• Found hole: _ :: [Char] -> [String]
• In the expression: _
In the expression: (_ "hello") :: [String]
In an equation for ‘it’: it = (_ "hello") :: [String]
• Relevant bindings include
it :: [String] (bound at <interactive>:1:1)
Valid hole fits include
lines :: String -> [String]
words :: String -> [String]
repeat :: forall a. a -> [a]
with a ~ String
fail :: forall (m :: * -> *) a. Monad m => String -> m a
with m ~ [], a ~ String
return :: forall (m :: * -> *) a. Monad m => a -> m a
with m ~ [], a ~ String
pure :: forall (f :: * -> *) a. Applicative f => a -> f a
with f ~ [], a ~ String
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
(0.14 secs,)
λ> :!color Lens.hs
-- Just to make sure this is off, in case I forget :)
{-# OPTIONS_GHC -frefinement-level-hole-fits=0 #-}
import Control.Lens
import Control.Monad.State
newtype T = T { _v :: Int }
val :: Lens' T Int
val f (T i) = T <$> f i
updT :: T -> T
updT t = t &~ do
val `_` (1 :: Int)
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ> :load Lens.hs
[1 of 1] Compiling Main ( Lens.hs, interpreted )
Lens.hs:13:3: error:
• Ambiguous type variable ‘f0’ arising from a use of ‘val’
prevents the constraint ‘(Functor f0)’ from being solved.
Probable fix: use a type annotation to specify what ‘f0’ should be.
These potential instances exist:
instance Functor (Either a) -- Defined in ‘Data.Either’
instance Functor Identity -- Defined in ‘Data.Functor.Identity’
instance Functor IO -- Defined in ‘GHC.Base’
...plus 14 others
...plus 154 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘_’, namely ‘val’
In a stmt of a 'do' block: val `_` (1 :: Int)
In the second argument of ‘(&~)’, namely ‘do val `_` (1 :: Int)’
|
13 | val `_` (1 :: Int)
| ^^^
Lens.hs:13:7: error:
• Found hole:
_ :: ((Int -> f0 Int) -> T -> f0 T) -> Int -> State T a0
Where: ‘f0’ is an ambiguous type variable
‘a0’ is an ambiguous type variable
• In the expression: _
In a stmt of a 'do' block: val `_` (1 :: Int)
In the second argument of ‘(&~)’, namely ‘do val `_` (1 :: Int)’
• Relevant bindings include
t :: T (bound at Lens.hs:12:6)
updT :: T -> T (bound at Lens.hs:12:1)
Valid hole fits include
(#=) :: forall s (m :: * -> *) a b.
MonadState s m =>
ALens s s a b -> b -> m ()
with s ~ T, m ~ (StateT T Identity), a ~ Int, b ~ Int
(<#=) :: forall s (m :: * -> *) a b.
MonadState s m =>
ALens s s a b -> b -> m b
with s ~ T, m ~ (StateT T Identity), a ~ Int, b ~ Int
(<*=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<+=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<-=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(<<*=) :: forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
with s ~ T, m ~ (StateT T Identity), a ~ Int
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
|
13 | val `_` (1 :: Int)
| ^^^
Failed, no modules loaded.
(0.76 secs,)
λ> _ :: [a] -> a
<interactive>:12:1: error:
• Found hole: _ :: [a1] -> a1
Where: ‘a1’ is a rigid type variable bound by
an expression type signature:
forall a1. [a1] -> a1
at <interactive>:12:6-13
• In the expression: _ :: [a] -> a
In an equation for ‘it’: it = _ :: [a] -> a
• Relevant bindings include
it :: [a] -> a (bound at <interactive>:12:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ a1
last :: forall a. [a] -> a
with a ~ a1
(0.17 secs,)
λ>
λ>
λ> _ :: Num a => [a] -> a
<interactive>:15:1: error:
• Found hole: _ :: [a1] -> a1
Where: ‘a1’ is a rigid type variable bound by
an expression type signature:
forall a1. Num a1 => [a1] -> a1
at <interactive>:15:6-22
• In the expression: _ :: Num a => [a] -> a
In an equation for ‘it’: it = _ :: Num a => [a] -> a
• Relevant bindings include
it :: [a] -> a (bound at <interactive>:15:1)
Constraints include
Num a1 (from <interactive>:15:6-22)
Num a (from <interactive>:15:1-22)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ a1
last :: forall a. [a] -> a
with a ~ a1
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ a1
sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ a1
(0.17 secs,)
λ>
λ>
λ>
λ>
λ> _ :: Ord a => [a] -> a
<interactive>:20:1: error:
• Found hole: _ :: [a1] -> a1
Where: ‘a1’ is a rigid type variable bound by
an expression type signature:
forall a1. Ord a1 => [a1] -> a1
at <interactive>:20:6-22
• In the expression: _ :: Ord a => [a] -> a
In an equation for ‘it’: it = _ :: Ord a => [a] -> a
• Relevant bindings include
it :: [a] -> a (bound at <interactive>:20:1)
Constraints include
Ord a1 (from <interactive>:20:6-22)
Ord a (from <interactive>:20:1-22)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ a1
last :: forall a. [a] -> a
with a ~ a1
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ a1
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ a1
(0.14 secs,)
λ>
λ>
λ>
λ>
λ> _ :: [Int] -> Int
<interactive>:25:1: error:
• Found hole: _ :: [Int] -> Int
• In the expression: _ :: [Int] -> Int
In an equation for ‘it’: it = _ :: [Int] -> Int
• Relevant bindings include
it :: [Int] -> Int (bound at <interactive>:25:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ Int
last :: forall a. [a] -> a
with a ~ Int
length :: forall (t :: * -> *) a. Foldable t => t a -> Int
with t ~ [], a ~ Int
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ Int
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
(0.08 secs,)
λ>
λ>
λ>
λ> :set -frefinement-level-hole-fits=1
λ>
λ>
λ>
λ> _ :: [Int] -> Int
<interactive>:33:1: error:
• Found hole: _ :: [Int] -> Int
• In the expression: _ :: [Int] -> Int
In an equation for ‘it’: it = _ :: [Int] -> Int
• Relevant bindings include
it :: [Int] -> Int (bound at <interactive>:33:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ Int
last :: forall a. [a] -> a
with a ~ Int
length :: forall (t :: * -> *) a. Foldable t => t a -> Int
with t ~ [], a ~ Int
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ Int
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
Valid refinement hole fits include
foldl1 (_ :: Int -> Int -> Int)
where foldl1 :: forall (t :: * -> *) a.
Foldable t =>
(a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
foldr1 (_ :: Int -> Int -> Int)
where foldr1 :: forall (t :: * -> *) a.
Foldable t =>
(a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
const (_ :: Int)
where const :: forall a b. a -> b -> a
with a ~ Int, b ~ [Int]
($) (_ :: [Int] -> Int)
where ($) :: forall a b. (a -> b) -> a -> b
with r ~ 'GHC.Types.LiftedRep, a ~ [Int], b ~ Int
fail (_ :: String)
where fail :: forall (m :: * -> *) a. Monad m => String -> m a
with m ~ ((->) [Int]), a ~ Int
return (_ :: Int)
where return :: forall (m :: * -> *) a. Monad m => a -> m a
with m ~ ((->) [Int]), a ~ Int
(Some refinement hole fits suppressed; use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)
(0.17 secs,)
λ> :set -frefinement-level-hole-fits=2
λ> _ :: [Int] -> Int
<interactive>:35:1: error:
• Found hole: _ :: [Int] -> Int
• In the expression: _ :: [Int] -> Int
In an equation for ‘it’: it = _ :: [Int] -> Int
• Relevant bindings include
it :: [Int] -> Int (bound at <interactive>:35:1)
Valid hole fits include
head :: forall a. [a] -> a
with a ~ Int
last :: forall a. [a] -> a
with a ~ Int
length :: forall (t :: * -> *) a. Foldable t => t a -> Int
with t ~ [], a ~ Int
maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
with t ~ [], a ~ Int
product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
with t ~ [], a ~ Int
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
Valid refinement hole fits include
foldl1 (_ :: Int -> Int -> Int)
where foldl1 :: forall (t :: * -> *) a.
Foldable t =>
(a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
foldr1 (_ :: Int -> Int -> Int)
where foldr1 :: forall (t :: * -> *) a.
Foldable t =>
(a -> a -> a) -> t a -> a
with t ~ [], a ~ Int
foldl (_ :: Int -> Int -> Int) (_ :: Int)
where foldl :: forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
with t ~ [], b ~ Int, a ~ Int
foldr (_ :: Int -> Int -> Int) (_ :: Int)
where foldr :: forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
with t ~ [], a ~ Int, b ~ Int
const (_ :: Int)
where const :: forall a b. a -> b -> a
with a ~ Int, b ~ [Int]
($) (_ :: [Int] -> Int)
where ($) :: forall a b. (a -> b) -> a -> b
with r ~ 'GHC.Types.LiftedRep, a ~ [Int], b ~ Int
(Some refinement hole fits suppressed; use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)
(0.27 secs,)
λ> :set -fre
-freduction-depth -fregs-graph -freverse-errors
-frefinement-level-hole-fits -fregs-iterative
λ> :set -frefinement-level-hole-fits=0
λ> :!color Richard.hs
{-# LANGUAGE ScopedTypeVariables #-}
module Richard where
prefix :: forall a . a -> [[a]] -> [[a]]
prefix x yss = map _a yss
where xcons :: [a] -> [a]
xcons ys = _a : ys
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ> :load Richard.hs
[1 of 1] Compiling Richard ( Richard.hs, interpreted )
Richard.hs:5:20: error:
• Found hole: _a :: [a] -> [a]
Where: ‘a’ is a rigid type variable bound by
the type signature for:
prefix :: forall a. a -> [[a]] -> [[a]]
at Richard.hs:4:1-40
Or perhaps ‘_a’ is mis-spelled, or not in scope
• In the first argument of ‘map’, namely ‘_a’
In the expression: map _a yss
In an equation for ‘prefix’:
prefix x yss
= map _a yss
where
xcons :: [a] -> [a]
xcons ys = _a : ys
• Relevant bindings include
xcons :: [a] -> [a] (bound at Richard.hs:7:9)
yss :: [[a]] (bound at Richard.hs:5:10)
x :: a (bound at Richard.hs:5:8)
prefix :: a -> [[a]] -> [[a]] (bound at Richard.hs:5:1)
Valid hole fits include
xcons :: [a] -> [a]
cycle :: forall a. [a] -> [a]
with a ~ a
init :: forall a. [a] -> [a]
with a ~ a
reverse :: forall a. [a] -> [a]
with a ~ a
tail :: forall a. [a] -> [a]
with a ~ a
id :: forall a. a -> a
with a ~ [a]
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
|
5 | prefix x yss = map _a yss
| ^^
Richard.hs:7:20: error:
• Found hole: _a :: a
Where: ‘a’ is a rigid type variable bound by
the type signature for:
prefix :: forall a. a -> [[a]] -> [[a]]
at Richard.hs:4:1-40
Or perhaps ‘_a’ is mis-spelled, or not in scope
• In the first argument of ‘(:)’, namely ‘_a’
In the expression: _a : ys
In an equation for ‘xcons’: xcons ys = _a : ys
• Relevant bindings include
ys :: [a] (bound at Richard.hs:7:15)
xcons :: [a] -> [a] (bound at Richard.hs:7:9)
yss :: [[a]] (bound at Richard.hs:5:10)
x :: a (bound at Richard.hs:5:8)
prefix :: a -> [[a]] -> [[a]] (bound at Richard.hs:5:1)
Valid hole fits include x :: a
|
7 | xcons ys = _a : ys
| ^^
Failed, no modules loaded.
(0.13 secs,)
λ> :!color Sorting.hs
{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, TypeApplications #-}
module Sorting ( mergeSort, quickSort, insertionSort
, Sorted, runSort, module ONotation) where
import ONotation
import Data.Type.Bool
import Data.Type.Equality
import Data.List (insert, sort, partition, foldl')
-- Sorted encodes average computational and auxiliary memory complexity.
-- The complexities presented here are the in-place complexities,
-- and do not match the naive but concise implementations included here.
newtype Sorted (cpu :: AsymP) (mem :: AsymP) a = Sorted {runSort :: [a]}
insertionSort :: (n >=. O(N^.2), m >=. O(One), Ord a) => [a] -> Sorted n m a
insertionSort = Sorted . foldl' (flip insert) []
mergeSort :: (n >=. O(N*.LogN), m >=. O(N), Ord a) => [a] -> Sorted n m a
mergeSort = Sorted . sort
quickSort :: (n >=. O(N*.LogN) , m >=. O(LogN), Ord a) => [a] -> Sorted n m a
quickSort (x:xs) = Sorted $ (recr lt) ++ (x:(recr gt))
where (lt, gt) = partition (< x) xs
recr = runSort . quickSort @(O(N*.LogN)) @(O(LogN))
quickSort [] = Sorted []
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ> _ [3,2,1] :: Sorted (O(N*.LogN)) (O(N)) Integer
<interactive>:58:14: error:
Not in scope: type constructor or class ‘Sorted’
<interactive>:58:22: error:
Not in scope: type constructor or class ‘O’
<interactive>:58:24: error:
Not in scope: type constructor or class ‘N’
<interactive>:58:25: error:
Not in scope: type constructor or class ‘*.’
<interactive>:58:27: error:
Not in scope: type constructor or class ‘LogN’
<interactive>:58:35: error:
Not in scope: type constructor or class ‘O’
<interactive>:58:37: error:
Not in scope: type constructor or class ‘N’
(0.01 secs,)
λ> :load Sorting.hs
[1 of 2] Compiling ONotation ( ONotation.hs, interpreted )
[2 of 2] Compiling Sorting ( Sorting.hs, interpreted )
Ok, two modules loaded.
(0.03 secs,)
λ> _ [3,2,1] :: Sorted (O(N*.LogN)) (O(N)) Integer
<interactive>:60:1: error:
• Found hole:
_ :: [Integer] -> Sorted (O ('NLogN 1 1)) (O N) Integer
• In the expression: _
In the expression:
_ [3, 2, 1] :: Sorted (O (N *. LogN)) (O (N)) Integer
In an equation for ‘it’:
it = _ [3, 2, ....] :: Sorted (O (N *. LogN)) (O (N)) Integer
• Relevant bindings include
it :: Sorted (O (N *. LogN)) (O N) Integer
(bound at <interactive>:60:1)
Valid hole fits include
mergeSort :: forall (n :: AsymP) (m :: AsymP) a.
(n >=. O (N *. LogN), m >=. O N, Ord a) =>
[a] -> Sorted n m a
with n ~ (O ('NLogN 1 1)), m ~ (O N), a ~ Integer
quickSort :: forall (n :: AsymP) (m :: AsymP) a.
(n >=. O (N *. LogN), m >=. O LogN, Ord a) =>
[a] -> Sorted n m a
with n ~ (O ('NLogN 1 1)), m ~ (O N), a ~ Integer
Sorted :: forall (cpu :: AsymP) (mem :: AsymP) a.
[a] -> Sorted cpu mem a
with cpu ~ (O ('NLogN 1 1)), mem ~ (O N), a ~ Integer
(0.10 secs,)
λ> _ [3,2,1] :: Sorted (O(N)) (O(N)) Integer
<interactive>:61:1: error:
• Found hole: _ :: [Integer] -> Sorted (O N) (O N) Integer
• In the expression: _
In the expression: _ [3, 2, 1] :: Sorted (O (N)) (O (N)) Integer
In an equation for ‘it’:
it = _ [3, 2, ....] :: Sorted (O (N)) (O (N)) Integer
• Relevant bindings include
it :: Sorted (O N) (O N) Integer (bound at <interactive>:61:1)
Valid hole fits include
Sorted :: forall (cpu :: AsymP) (mem :: AsymP) a.
[a] -> Sorted cpu mem a
with cpu ~ (O N), mem ~ (O N), a ~ Integer
(0.08 secs,)
λ> :!color Free.hs
module Free where
data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Functor (Free f) where
fmap f = go where
go (Pure a) = Pure (f a)
go (Free fa) = Free (go <$> fa)
instance Functor f => Applicative (Free f) where
pure = Pure
Pure a <*> Pure b = Pure $ a b
Pure a <*> Free mb = Free $ fmap a <$> mb
Free ma <*> b = Free $ (<*> b) <$> ma
instance Functor f => Monad (Free f) where
return = pure
Pure a >>= f = f a
Free m >>= f = Free (fmap _ m)
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ>
λ> :load Free.hs
[1 of 1] Compiling Free ( Free.hs, interpreted )
Free.hs:22:29: error:
• Found hole: _ :: Free f a -> Free f b
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
(>>=) :: forall a b. Free f a -> (a -> Free f b) -> Free f b
at Free.hs:21:10-12
‘f’ is a rigid type variable bound by
the instance declaration
at Free.hs:18:10-36
• In the first argument of ‘fmap’, namely ‘_’
In the first argument of ‘Free’, namely ‘(fmap _ m)’
In the expression: Free (fmap _ m)
• Relevant bindings include
f :: a -> Free f b (bound at Free.hs:22:14)
m :: f (Free f a) (bound at Free.hs:22:8)
(>>=) :: Free f a -> (a -> Free f b) -> Free f b
(bound at Free.hs:21:10)
Constraints include Functor f (from Free.hs:18:10-36)
|
22 | Free m >>= f = Free (fmap _ m)
| ^
Failed, no modules loaded.
(0.05 secs,)
λ> :set -frefinement-level-hole-fits=1
λ> :load Free.hs
[1 of 1] Compiling Free ( Free.hs, interpreted )
Free.hs:22:29: error:
• Found hole: _ :: Free f a -> Free f b
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
(>>=) :: forall a b. Free f a -> (a -> Free f b) -> Free f b
at Free.hs:21:10-12
‘f’ is a rigid type variable bound by
the instance declaration
at Free.hs:18:10-36
• In the first argument of ‘fmap’, namely ‘_’
In the first argument of ‘Free’, namely ‘(fmap _ m)’
In the expression: Free (fmap _ m)
• Relevant bindings include
f :: a -> Free f b (bound at Free.hs:22:14)
m :: f (Free f a) (bound at Free.hs:22:8)
(>>=) :: Free f a -> (a -> Free f b) -> Free f b
(bound at Free.hs:21:10)
Constraints include Functor f (from Free.hs:18:10-36)
Valid refinement hole fits include
fmap (_ :: a -> b)
where fmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f a -> f b
with f ~ (Free f), a ~ a, b ~ b
(<*>) (_ :: Free f (a -> b))
where (<*>) :: forall (f :: * -> *) a b.
Applicative f =>
f (a -> b) -> f a -> f b
with f ~ (Free f), a ~ a, b ~ b
(=<<) (_ :: a -> Free f b)
where (=<<) :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m a -> m b
with m ~ (Free f), a ~ a, b ~ b
(<*) (_ :: Free f b)
where (<*) :: forall (f :: * -> *) a b.
Applicative f =>
f a -> f b -> f a
with f ~ (Free f), a ~ b, b ~ a
(<$) (_ :: b)
where (<$) :: forall (f :: * -> *) a b.
Functor f =>
a -> f b -> f a
with f ~ (Free f), a ~ b, b ~ a
(<$>) (_ :: a -> b)
where (<$>) :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f a -> f b
with f ~ (Free f), a ~ a, b ~ b
(Some refinement hole fits suppressed; use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)
|
22 | Free m >>= f = Free (fmap _ m)
| ^
Failed, no modules loaded.
(0.09 secs,)
λ>
λ>