-
-
Save mizunashi-mana/4522da17c8ade08b3376b1596c06be72 to your computer and use it in GitHub Desktop.
module Main where | |
dict Integral a = Integral { | |
fromInteger: Integer -> a, | |
+: a -> a -> a, | |
-: a -> a -> a, | |
iszero: a -> Bool, | |
} | |
impl integralForInteger: Integral Integer | |
integralForInteger = Integral have | |
fromInteger x = x | |
x + y = x Main.+ y | |
x - y = x Main.- y | |
iszero = \ | |
0 -> True | |
_ -> False | |
fromInteger: forall a. Integral a => Integer -> a | |
fromInteger %d = d.fromInteger | |
module Fib begin | |
fib: forall a. Integral a => a -> a | |
fib @a %d n = go n a0 a1 | |
where | |
a0 = fromInteger %integralForInteger 0 | |
a1 = fromInteger 1 -- implicit dictionary inference | |
-- `go` can have a signature `go: a -> a -> a -> a` | |
go m x y = \ | |
| d.iszero m -> x | |
| else -> go (m - 1) y (x d.+ y) | |
end | |
main: IO () | |
main = print $ Fib.fib 10 |
in strict language, A { a = undefined } = A undefined = undefined, so in pure $ f %defA, you're basically passing undefined into f - just the fact that it's passed here as an argument is reason for it to panic.
This is not the unique solution and I expect A { a = undefined }
is a normal form as Main { f = undefined }
is not diverge if A
is a dictionary constructor (module constructor).
When it comes to decidability in instance search, it isn't really that useful in non-total language
In many cases, decidability in instance search is related compile performance directly. I agree with it isn't useful for language user. However, it is important for language provider because instance search may be bottleneck. And, it is a choice to restrict instance form for compile performance although it may make language power is weaker.
This is not the unique solution and I expect A { a = undefined } is a normal form as Main { f = undefined } is not diverge if A is a dictionary constructor (module constructor).
Alright, so you want modules/dictionaries to behave in a specific way. Yeah, then they aren't ordinary values after all.
In many cases, decidability in instance search is related compile performance directly. I agree with it isn't useful for language user. However, it is important for language provider because instance search may be bottleneck. And, it is a choice to restrict instance form for compile performance although it may make language power is weaker.
Part of GHC's manual about overlapping instances describes how instance search works in GHC, plus part about UndecidableInstances
mentions that it's used to lift "rules that ensure that instance resolution will terminate". I don't see any mention about performance effect in either of these, neither I'm sure how ensuring termination of instance search can help performance directly - but maybe you can point me to some useful material.
In many cases, algorithms for undecidable problem are unpredictable; this is from my experience and not principle.
In many cases, decidability in instance search is related compile performance directly.
may have mistake, sorry. Correctly, guarantee of decidability of instance search is important for language designer to maintain the compiler.
Decidability of instance search is more generic concept. A group of instances with cyclic super context is just one of undecidability. Haskell have special syntax for class and instance declaration and the designers of the language thought decidability of instance resolution deeply. Then, undecidable problem of instance resolution in Haskell is just "cyclic context". However, we can choose another design that the instance resolution of our language is turing complete (e.g. arithmetic expression is allowed). This is expressive but compile time depends strongly on the program.
Scala has powerful instance searcher which is a solution of undecidable problem. However, it is a troublemaker for compile performance.
This diverges - when it's used somewhere.
Yes.
This
main
should - in strict language,A { a = undefined } = A undefined = undefined
, so inpure $ f %defA
, you're basically passingundefined
intof
- just the fact that it's passed here as an argument is reason for it to panic. BTW, in strict language,seq
should be no-op - you never get thunk to evaluate, argument of some typea
is evaluated value of such type, not a computation that produces it.When it comes to decidability in instance search, it isn't really that useful in non-total language - if it gets stuck, it will happen at compile-time, not runtime, plus we're already disabling it in Haskell in many cases.